λn1. λn2. λp1. λp2. λf1. λf2. ex (λh. ex (λk. ((∀ i, i < n1 ⇒ (p1 i) = true ⇒ (f1 i) = (f2 (h i))) ∧ (sub_hk h k n1 n2 p1 p2 f1 f2)) ∧ (sub_hk k h n2 n1 p2 p1 f2 f1)))

Definition iso : nat.nat -> nat.nat -> (nat.nat -> bool.bool) -> (nat.nat -> bool.bool) -> (nat.nat -> nat.nat) -> (nat.nat -> nat.nat) -> Prop := fun (n1:nat.nat) => fun (n2:nat.nat) => fun (p1:(nat.nat -> bool.bool)) => fun (p2:(nat.nat -> bool.bool)) => fun (f1:(nat.nat -> nat.nat)) => fun (f2:(nat.nat -> nat.nat)) => connectives.ex (nat.nat -> nat.nat) (fun (h:(nat.nat -> nat.nat)) => connectives.ex (nat.nat -> nat.nat) (fun (k:(nat.nat -> nat.nat)) => connectives.And (connectives.And (forall (i:nat.nat), (nat.lt i n1) -> (logic.eq (bool.bool) (p1 i) bool.true) -> logic.eq (nat.nat) (f1 i) (f2 (h i))) (sub_hk h k n1 n2 p1 p2 f1 f2)) (sub_hk k h n2 n1 p2 p1 f2 f1)))

definition iso : nat -> nat -> (nat -> bool) -> (nat -> bool) -> (nat -> nat) -> (nat -> nat) -> Prop := \lambda n1 : nat. \lambda n2 : nat. \lambda p1 : nat -> bool. \lambda p2 : nat -> bool. \lambda f1 : nat -> nat. \lambda f2 : nat -> nat. (ex) (nat -> nat) (\lambda h : nat -> nat. (ex) (nat -> nat) (\lambda k : nat -> nat. (And) ((And) (\forall (i:nat). ((lt) i n1) -> ((eq) (bool) (p1 i) (true) ) -> (eq) (nat) (f1 i) (f2 (h i))) ((sub_hk) h k n1 n2 p1 p2 f1 f2)) ((sub_hk) k h n2 n1 p2 p1 f2 f1)))

def iso : (nat.nat) -> (nat.nat) -> ((nat.nat) -> bool.bool) -> ((nat.nat) -> bool.bool) -> ((nat.nat) -> nat.nat) -> ((nat.nat) -> nat.nat) -> Prop := fun (n1 : nat.nat) , fun (n2 : nat.nat) , fun (p1 : (nat.nat) -> bool.bool) , fun (p2 : (nat.nat) -> bool.bool) , fun (f1 : (nat.nat) -> nat.nat) , fun (f2 : (nat.nat) -> nat.nat) , ((connectives.ex) ((nat.nat) -> nat.nat)) (fun (h : (nat.nat) -> nat.nat) , ((connectives.ex) ((nat.nat) -> nat.nat)) (fun (k : (nat.nat) -> nat.nat) , (((connectives.And) ) ((((connectives.And) ) (forall (i:nat.nat) , ((((nat.lt_) ) (i)) (n1)) -> ((((logic.eq_) (bool.bool)) ((p1) (i))) ((bool.true) )) -> (((logic.eq_) (nat.nat)) ((f1) (i))) ((f2) ((h) (i))))) ((((((((((bigops.sub_hk) ) (h)) (k)) (n1)) (n2)) (p1)) (p2)) (f1)) (f2)))) ((((((((((bigops.sub_hk) ) (k)) (h)) (n2)) (n1)) (p2)) (p1)) (f2)) (f1))))

iso : [nat_sttfa_th.sttfa_nat -> [nat_sttfa_th.sttfa_nat -> [[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool] -> [[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool] -> [[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat] -> [[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat] -> bool]]]]]] = (LAMBDA(n1:nat_sttfa_th.sttfa_nat):(LAMBDA(n2:nat_sttfa_th.sttfa_nat):(LAMBDA(p1:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(LAMBDA(p2:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(LAMBDA(f1:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(LAMBDA(f2:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):connectives_sttfa_th.sttfa_ex[[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]]((LAMBDA(h:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):connectives_sttfa_th.sttfa_ex[[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]]((LAMBDA(k:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):connectives_sttfa_th.sttfa_And(connectives_sttfa_th.sttfa_And((FORALL(i:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(i)(n1) => (logic_sttfa_th.eq[bool_sttfa_th.sttfa_bool](p1(i))(bool_sttfa_th.sttfa_true) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](f1(i))(f2(h(i)))))))(bigops_sttfa.sub_hk(h)(k)(n1)(n2)(p1)(p2)(f1)(f2)))(bigops_sttfa.sub_hk(k)(h)(n2)(n1)(p2)(p1)(f2)(f1))))))))))))

Printing for OpenTheory is not working at the moment.