∀ e p n m, n ≤ m ⇒ sub_hk (λx. x) (λx. x) n m p p e e

Theorem sub_lt : forall (e:(nat.nat -> nat.nat)), forall (p:(nat.nat -> bool.bool)), forall (n:nat.nat), forall (m:nat.nat), (nat.le n m) -> sub_hk (fun (x:nat.nat) => x) (fun (x:nat.nat) => x) n m p p e e.

theorem sub_lt : \forall (e:nat -> nat). \forall (p:nat -> bool). \forall (n:nat). \forall (m:nat). ((le) n m) -> (sub_hk) (\lambda x : nat. x) (\lambda x : nat. x) n m p p e e.

theorem sub_lt : forall (e:(nat.nat) -> nat.nat) , forall (p:(nat.nat) -> bool.bool) , forall (n:nat.nat) , forall (m:nat.nat) , ((((nat.le_) ) (n)) (m)) -> (((((((((bigops.sub_hk) ) (fun (x : nat.nat) , x)) (fun (x : nat.nat) , x)) (n)) (m)) (p)) (p)) (e)) (e).

sub_lt : LEMMA (FORALL(e:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(p:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.le(n)(m) => bigops_sttfa.sub_hk((LAMBDA(x:nat_sttfa_th.sttfa_nat):x))((LAMBDA(x:nat_sttfa_th.sttfa_nat):x))(n)(m)(p)(p)(e)(e))))))

Printing for OpenTheory is not working at the moment.