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

Definition sub_hk : (nat.nat -> nat.nat) -> (nat.nat -> nat.nat) -> nat.nat -> nat.nat -> (nat.nat -> bool.bool) -> (nat.nat -> bool.bool) -> (nat.nat -> nat.nat) -> (nat.nat -> nat.nat) -> Prop := fun (h:(nat.nat -> nat.nat)) => fun (k:(nat.nat -> nat.nat)) => 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)) => forall (i:nat.nat), (nat.lt i n1) -> (logic.eq (bool.bool) (p1 i) bool.true) -> connectives.And (connectives.And (nat.lt (h i) n2) (logic.eq (bool.bool) (p2 (h i)) bool.true)) (logic.eq (nat.nat) (k (h i)) i)

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

def sub_hk : ((nat.nat) -> nat.nat) -> ((nat.nat) -> nat.nat) -> (nat.nat) -> (nat.nat) -> ((nat.nat) -> bool.bool) -> ((nat.nat) -> bool.bool) -> ((nat.nat) -> nat.nat) -> ((nat.nat) -> nat.nat) -> Prop := fun (h : (nat.nat) -> nat.nat) , fun (k : (nat.nat) -> nat.nat) , 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) , forall (i:nat.nat) , ((((nat.lt_) ) (i)) (n1)) -> ((((logic.eq_) (bool.bool)) ((p1) (i))) ((bool.true) )) -> (((connectives.And) ) ((((connectives.And) ) ((((nat.lt_) ) ((h) (i))) (n2))) ((((logic.eq_) (bool.bool)) ((p2) ((h) (i)))) ((bool.true) )))) ((((logic.eq_) (nat.nat)) ((k) ((h) (i)))) (i))

sub_hk : [[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat] -> [[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat] -> [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(h:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(LAMBDA(k:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(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]):(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) => connectives_sttfa_th.sttfa_And(connectives_sttfa_th.sttfa_And(nat_sttfa_th.lt(h(i))(n2))(logic_sttfa_th.eq[bool_sttfa_th.sttfa_bool](p2(h(i)))(bool_sttfa_th.sttfa_true)))(logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](k(h(i)))(i)))))))))))))

Printing for OpenTheory is not working at the moment.