∀ p f g n m, n ≤ m ⇒ sameF_p m p f g ⇒ sameF_p n p f g

Theorem sameF_p_le : forall A, forall (p:(nat.nat -> bool.bool)), forall (f:(nat.nat -> A)), forall (g:(nat.nat -> A)), forall (n:nat.nat), forall (m:nat.nat), (nat.le n m) -> (sameF_p (A) m p f g) -> sameF_p (A) n p f g.

theorem sameF_p_le : \forall A. \forall (p:nat -> bool). \forall (f:nat -> A). \forall (g:nat -> A). \forall (n:nat). \forall (m:nat). ((le) n m) -> ((sameF_p) (A) m p f g) -> (sameF_p) (A) n p f g.

theorem sameF_p_le : forall (A : Type) , forall (p:(nat.nat) -> bool.bool) , forall (f:(nat.nat) -> A) , forall (g:(nat.nat) -> A) , forall (n:nat.nat) , forall (m:nat.nat) , ((((nat.le_) ) (n)) (m)) -> ((((((bigops.sameF_p) (A)) (m)) (p)) (f)) (g)) -> (((((bigops.sameF_p) (A)) (n)) (p)) (f)) (g).

sameF_p_le [A:TYPE+] : LEMMA (FORALL(p:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(FORALL(f:[nat_sttfa_th.sttfa_nat -> A]):(FORALL(g:[nat_sttfa_th.sttfa_nat -> A]):(FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.le(n)(m) => (bigops_sttfa.sameF_p[A](m)(p)(f)(g) => bigops_sttfa.sameF_p[A](n)(p)(f)(g))))))))

Printing for OpenTheory is not working at the moment.