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

Theorem

nat.sym_eq_match_nat_type_O

Statement

∀ case_O case_S, leibniz case_O (match_nat_type case_O case_S O)

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem sym_eq_match_nat_type_O : forall return_type, forall (case_O:return_type), forall (case_S:(nat -> return_type)), leibniz.leibniz (return_type) case_O (match_nat_type (return_type) case_O case_S O).



Matita-Jumb
Statement

theorem sym_eq_match_nat_type_O : \forall return_type. \forall (case_O:return_type). \forall (case_S:nat -> return_type). (leibniz) (return_type) case_O ((match_nat_type) (return_type) case_O case_S (O) ).



Lean-jumb
Statement

theorem sym_eq_match_nat_type_O : forall (return_type : Type) , forall (case_O:return_type) , forall (case_S:(nat.nat) -> return_type) , (((leibniz.leibniz) (return_type)) (case_O)) (((((nat.match_nat_type) (return_type)) (case_O)) (case_S)) ((nat.O) )).



PVS-jumb

Statement

sym_eq_match_nat_type_O [return_type:TYPE+] : LEMMA (FORALL(case_O:return_type):(FORALL(case_S:[nat_sttfa.sttfa_nat -> return_type]):leibniz_sttfa_th.leibniz[return_type](case_O)(nat_sttfa.match_nat_type[return_type](case_O)(case_S)(nat_sttfa.sttfa_O))))



OpenTheory

Printing for OpenTheory is not working at the moment.