∀ H, nat.nat → (nat.nat → bool.bool) → H → (H → H → H) → (nat.nat → H) → H

Parameter bigop_body : forall (H:Type), nat.nat -> (nat.nat -> bool.bool) -> H -> (H -> H -> H) -> (nat.nat -> H) -> H

axiom bigop_body : \forall H : Type[0] . nat -> (nat -> bool) -> H -> (H -> H -> H) -> (nat -> H) -> H

constant bigop_body : forall (H : Type) , (nat.nat) -> ((nat.nat) -> bool.bool) -> (H) -> ((H) -> (H) -> H) -> ((nat.nat) -> H) -> H

bigop_body [H:TYPE+] : [nat_sttfa_th.sttfa_nat -> [[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool] -> [H -> [[H -> [H -> H]] -> [[nat_sttfa_th.sttfa_nat -> H] -> H]]]]]

Printing for OpenTheory is not working at the moment.