def or_false_right

stelliferous@0.0.2.0 · proofs/boolean_logic.bend:86

import Base
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

86def or_false_right(+first: Bool,+second: Bool,proof: {first || second == False{} : Bool}) -> {second == False{} : Bool}:
87  match first:
88    case False{}: proof
89    case True{}: Empty.absurd({second == False{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},proof)))