λk. λp. λf. λg. ∀ i, i < k ⇒ (p i) = true ⇒ (f i) = (g i)

Definition sameF_p : forall (A:Type), nat.nat -> (nat.nat -> bool.bool) -> (nat.nat -> A) -> (nat.nat -> A) -> Prop := fun (A:Type) => fun (k:nat.nat) => fun (p:(nat.nat -> bool.bool)) => fun (f:(nat.nat -> A)) => fun (g:(nat.nat -> A)) => forall (i:nat.nat), (nat.lt i k) -> (logic.eq (bool.bool) (p i) bool.true) -> logic.eq (A) (f i) (g i)

definition sameF_p : \forall A : Type[0] . nat -> (nat -> bool) -> (nat -> A) -> (nat -> A) -> Prop := \lambda A : Type[0]. \lambda k : nat. \lambda p : nat -> bool. \lambda f : nat -> A. \lambda g : nat -> A. \forall (i:nat). ((lt) i k) -> ((eq) (bool) (p i) (true) ) -> (eq) (A) (f i) (g i)

def sameF_p : forall (A : Type) , (nat.nat) -> ((nat.nat) -> bool.bool) -> ((nat.nat) -> A) -> ((nat.nat) -> A) -> Prop := fun (A : Type) , fun (k : nat.nat) , fun (p : (nat.nat) -> bool.bool) , fun (f : (nat.nat) -> A) , fun (g : (nat.nat) -> A) , forall (i:nat.nat) , ((((nat.lt_) ) (i)) (k)) -> ((((logic.eq_) (bool.bool)) ((p) (i))) ((bool.true) )) -> (((logic.eq_) (A)) ((f) (i))) ((g) (i))

sameF_p [A:TYPE+] : [nat_sttfa_th.sttfa_nat -> [[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool] -> [[nat_sttfa_th.sttfa_nat -> A] -> [[nat_sttfa_th.sttfa_nat -> A] -> bool]]]] = (LAMBDA(k:nat_sttfa_th.sttfa_nat):(LAMBDA(p:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(LAMBDA(f:[nat_sttfa_th.sttfa_nat -> A]):(LAMBDA(g:[nat_sttfa_th.sttfa_nat -> A]):(FORALL(i:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(i)(k) => (logic_sttfa_th.eq[bool_sttfa_th.sttfa_bool](p(i))(bool_sttfa_th.sttfa_true) => logic_sttfa_th.eq[A](f(i))(g(i)))))))))

Printing for OpenTheory is not working at the moment.