// This prints the left floatting menu
Dedukti    Load Matita      Load Coq         Load Lean        Load PVS         Load OpenTheory Load
Dedukti-jumb

Axiom

bool.sym_eq_match_bool_type_false

Statement

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

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem sym_eq_match_bool_type_false : forall return_, forall (case_true:return_), forall (case_false:return_), leibniz.leibniz (return_) case_false (match_bool_type (return_) case_true case_false false).



Matita-Jumb
Statement

theorem sym_eq_match_bool_type_false : \forall return_. \forall (case_true:return_). \forall (case_false:return_). (leibniz) (return_) case_false ((match_bool_type) (return_) case_true case_false (false) ).



Lean-jumb
Statement

theorem sym_eq_match_bool_type_false : forall (return : Type) , forall (case_true:return) , forall (case_false:return) , (((leibniz.leibniz) (return)) (case_false)) (((((bool.match_bool_type) (return)) (case_true)) (case_false)) ((bool.false) )).



PVS-jumb

Statement

sym_eq_match_bool_type_false [return:TYPE+] : LEMMA (FORALL(case_true:return):(FORALL(case_false:return):leibniz_sttfa_th.leibniz[return](case_false)(bool_sttfa.match_bool_type[return](case_true)(case_false)(bool_sttfa.sttfa_false))))



OpenTheory

Printing for OpenTheory is not working at the moment.