∀ n, leibniz (bigop_body (n+1)) (bigop (n+1))

Theorem sym_eq_bigop_S : forall H, forall (n:nat.nat), leibniz.leibniz ((nat.nat -> bool.bool) -> H -> (H -> H -> H) -> (nat.nat -> H) -> H) (bigop_body (H) (nat.S n)) (bigop (H) (nat.S n)).

theorem sym_eq_bigop_S : \forall H. \forall (n:nat). (leibniz) ((nat -> bool) -> H -> (H -> H -> H) -> (nat -> H) -> H) ((bigop_body) (H) ((S) n)) ((bigop) (H) ((S) n)).

theorem sym_eq_bigop_S : forall (H : Type) , forall (n:nat.nat) , (((leibniz.leibniz) (((nat.nat) -> bool.bool) -> (H) -> ((H) -> (H) -> H) -> ((nat.nat) -> H) -> H)) (((bigops.bigop_body) (H)) (((nat.S) ) (n)))) (((bigops.bigop) (H)) (((nat.S) ) (n))).

sym_eq_bigop_S [H:TYPE+] : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):leibniz_sttfa_th.leibniz[[[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool] -> [H -> [[H -> [H -> H]] -> [[nat_sttfa_th.sttfa_nat -> H] -> H]]]]](bigops_sttfa.bigop_body[H](nat_sttfa_th.sttfa_S(n)))(bigops_sttfa.bigop[H](nat_sttfa_th.sttfa_S(n))))

Printing for OpenTheory is not working at the moment.