∀ case_true case_false, equal (if false then case_true else case_false) case_false

Axiom axiom_match_bool_type_false : forall return_, forall (case_true:return_), forall (case_false:return_), connectives.equal (return_) (match_bool_type (return_) case_true case_false false) case_false

axiom axiom_match_bool_type_false : \forall return_. \forall (case_true:return_). \forall (case_false:return_). (equal) (return_) ((match_bool_type) (return_) case_true case_false (false) ) case_false

axiom axiom_match_bool_type_false : forall (return : Type) , forall (case_true:return) , forall (case_false:return) , (((connectives.equal) (return)) (((((bool.match_bool_type) (return)) (case_true)) (case_false)) ((bool.false) ))) (case_false)

axiom_match_bool_type_false [return:TYPE+] : AXIOM (FORALL(case_true:return):(FORALL(case_false:return):connectives_sttfa_th.equal[return](bool_sttfa.match_bool_type[return](case_true)(case_false)(bool_sttfa.sttfa_false))(case_false)))

Printing for OpenTheory is not working at the moment.