def or_false_left
import stelliferous@0.0.2.0/proofs/boolean_logic.bend as BooleanLogicimport Base
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding
81def or_false_left(+first: Bool,+second: Bool,proof: {first || second == False{} : Bool}) -> {first == False{} : Bool}:
82 match first:
83 case False{}: {==}
84 case True{}: Empty.absurd({True{} == False{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},proof)))
Uses (5)
Used by (0)
No other definition uses this definition.