∀ h1 k1 h2 k2 n1 n2 n3 p1 p2 p3 f1 f2 f3, sub_hk h1 k1 n1 n2 p1 p2 f1 f2 ⇒ sub_hk h2 k2 n2 n3 p2 p3 f2 f3 ⇒ sub_hk (λx. h2 (h1 x)) (λx. k1 (k2 x)) n1 n3 p1 p3 f1 f3

Theorem transitive_sub : forall (h1:(nat.nat -> nat.nat)), forall (k1:(nat.nat -> nat.nat)), forall (h2:(nat.nat -> nat.nat)), forall (k2:(nat.nat -> nat.nat)), forall (n1:nat.nat), forall (n2:nat.nat), forall (n3:nat.nat), forall (p1:(nat.nat -> bool.bool)), forall (p2:(nat.nat -> bool.bool)), forall (p3:(nat.nat -> bool.bool)), forall (f1:(nat.nat -> nat.nat)), forall (f2:(nat.nat -> nat.nat)), forall (f3:(nat.nat -> nat.nat)), (sub_hk h1 k1 n1 n2 p1 p2 f1 f2) -> (sub_hk h2 k2 n2 n3 p2 p3 f2 f3) -> sub_hk (fun (x:nat.nat) => h2 (h1 x)) (fun (x:nat.nat) => k1 (k2 x)) n1 n3 p1 p3 f1 f3.

theorem transitive_sub : \forall (h1:nat -> nat). \forall (k1:nat -> nat). \forall (h2:nat -> nat). \forall (k2:nat -> nat). \forall (n1:nat). \forall (n2:nat). \forall (n3:nat). \forall (p1:nat -> bool). \forall (p2:nat -> bool). \forall (p3:nat -> bool). \forall (f1:nat -> nat). \forall (f2:nat -> nat). \forall (f3:nat -> nat). ((sub_hk) h1 k1 n1 n2 p1 p2 f1 f2) -> ((sub_hk) h2 k2 n2 n3 p2 p3 f2 f3) -> (sub_hk) (\lambda x : nat. h2 (h1 x)) (\lambda x : nat. k1 (k2 x)) n1 n3 p1 p3 f1 f3.

theorem transitive_sub : forall (h1:(nat.nat) -> nat.nat) , forall (k1:(nat.nat) -> nat.nat) , forall (h2:(nat.nat) -> nat.nat) , forall (k2:(nat.nat) -> nat.nat) , forall (n1:nat.nat) , forall (n2:nat.nat) , forall (n3:nat.nat) , forall (p1:(nat.nat) -> bool.bool) , forall (p2:(nat.nat) -> bool.bool) , forall (p3:(nat.nat) -> bool.bool) , forall (f1:(nat.nat) -> nat.nat) , forall (f2:(nat.nat) -> nat.nat) , forall (f3:(nat.nat) -> nat.nat) , ((((((((((bigops.sub_hk) ) (h1)) (k1)) (n1)) (n2)) (p1)) (p2)) (f1)) (f2)) -> ((((((((((bigops.sub_hk) ) (h2)) (k2)) (n2)) (n3)) (p2)) (p3)) (f2)) (f3)) -> (((((((((bigops.sub_hk) ) (fun (x : nat.nat) , (h2) ((h1) (x)))) (fun (x : nat.nat) , (k1) ((k2) (x)))) (n1)) (n3)) (p1)) (p3)) (f1)) (f3).

transitive_sub : LEMMA (FORALL(h1:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(k1:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(h2:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(k2:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(n1:nat_sttfa_th.sttfa_nat):(FORALL(n2:nat_sttfa_th.sttfa_nat):(FORALL(n3:nat_sttfa_th.sttfa_nat):(FORALL(p1:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(FORALL(p2:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(FORALL(p3:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(FORALL(f1:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(f2:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(f3:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(bigops_sttfa.sub_hk(h1)(k1)(n1)(n2)(p1)(p2)(f1)(f2) => (bigops_sttfa.sub_hk(h2)(k2)(n2)(n3)(p2)(p3)(f2)(f3) => bigops_sttfa.sub_hk((LAMBDA(x:nat_sttfa_th.sttfa_nat):h2(h1(x))))((LAMBDA(x:nat_sttfa_th.sttfa_nat):k1(k2(x))))(n1)(n3)(p1)(p3)(f1)(f3))))))))))))))))

Printing for OpenTheory is not working at the moment.