nat.sym_eq_match_nat_type_S
∀ case_O case_S n, leibniz (case_S n) (match_nat_type case_O case_S (n+1))
Theorem sym_eq_match_nat_type_S : forall return_type, forall (case_O:return_type), forall (case_S:(nat -> return_type)), forall (n:nat), leibniz.leibniz (return_type) (case_S n) (match_nat_type (return_type) case_O case_S (S n)).
theorem sym_eq_match_nat_type_S : \forall return_type. \forall (case_O:return_type). \forall (case_S:nat -> return_type). \forall (n:nat). (leibniz) (return_type) (case_S n) ((match_nat_type) (return_type) case_O case_S ((S) n)).
theorem sym_eq_match_nat_type_S : forall (return_type : Type) , forall (case_O:return_type) , forall (case_S:(nat.nat) -> return_type) , forall (n:nat.nat) , (((leibniz.leibniz) (return_type)) ((case_S) (n))) (((((nat.match_nat_type) (return_type)) (case_O)) (case_S)) (((nat.S) ) (n))).
sym_eq_match_nat_type_S [return_type:TYPE+] : LEMMA (FORALL(case_O:return_type):(FORALL(case_S:[nat_sttfa.sttfa_nat -> return_type]):(FORALL(n:nat_sttfa.sttfa_nat):leibniz_sttfa_th.leibniz[return_type](case_S(n))(nat_sttfa.match_nat_type[return_type](case_O)(case_S)(nat_sttfa.sttfa_S(n))))))
Printing for OpenTheory is not working at the moment.