equal (bigop_body O) (λp. λnil. λop. λf. nil)

Axiom axiom_bigop_body_O : forall H, connectives.equal ((nat.nat -> bool.bool) -> H -> (H -> H -> H) -> (nat.nat -> H) -> H) (bigop_body (H) nat.O) (fun (p:(nat.nat -> bool.bool)) => fun (nil:H) => fun (op:(H -> H -> H)) => fun (f:(nat.nat -> H)) => nil)

axiom axiom_bigop_body_O : \forall H. (equal) ((nat -> bool) -> H -> (H -> H -> H) -> (nat -> H) -> H) ((bigop_body) (H) (O) ) (\lambda p : nat -> bool. \lambda nil : H. \lambda op : H -> H -> H. \lambda f : nat -> H. nil)

axiom axiom_bigop_body_O : forall (H : Type) , (((connectives.equal) (((nat.nat) -> bool.bool) -> (H) -> ((H) -> (H) -> H) -> ((nat.nat) -> H) -> H)) (((bigops.bigop_body) (H)) ((nat.O) ))) (fun (p : (nat.nat) -> bool.bool) , fun (nil : H) , fun (op : (H) -> (H) -> H) , fun (f : (nat.nat) -> H) , nil)

axiom_bigop_body_O [H:TYPE+] : AXIOM connectives_sttfa_th.equal[[[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_O))((LAMBDA(p:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(LAMBDA(nil:H):(LAMBDA(op:[H -> [H -> H]]):(LAMBDA(f:[nat_sttfa_th.sttfa_nat -> H]):nil)))))

Printing for OpenTheory is not working at the moment.