∀ k p1 p2 nil op f g, sameF_upto k p1 p2 ⇒ sameF_p k p1 f g ⇒ (bigop k (λi. p1 i) nil op (λi. f i)) = (bigop k (λi. p2 i) nil op (λi. g i))

Theorem same_bigop : forall B, forall (k:nat.nat), forall (p1:(nat.nat -> bool.bool)), forall (p2:(nat.nat -> bool.bool)), forall (nil:B), forall (op:(B -> B -> B)), forall (f:(nat.nat -> B)), forall (g:(nat.nat -> B)), (sameF_upto (bool.bool) k p1 p2) -> (sameF_p (B) k p1 f g) -> logic.eq (B) (bigop (B) k (fun (i:nat.nat) => p1 i) nil op (fun (i:nat.nat) => f i)) (bigop (B) k (fun (i:nat.nat) => p2 i) nil op (fun (i:nat.nat) => g i)).

theorem same_bigop : \forall B. \forall (k:nat). \forall (p1:nat -> bool). \forall (p2:nat -> bool). \forall (nil:B). \forall (op:B -> B -> B). \forall (f:nat -> B). \forall (g:nat -> B). ((sameF_upto) (bool) k p1 p2) -> ((sameF_p) (B) k p1 f g) -> (eq) (B) ((bigop) (B) k (\lambda i : nat. p1 i) nil op (\lambda i : nat. f i)) ((bigop) (B) k (\lambda i : nat. p2 i) nil op (\lambda i : nat. g i)).

theorem same_bigop : forall (B : Type) , forall (k:nat.nat) , forall (p1:(nat.nat) -> bool.bool) , forall (p2:(nat.nat) -> bool.bool) , forall (nil:B) , forall (op:(B) -> (B) -> B) , forall (f:(nat.nat) -> B) , forall (g:(nat.nat) -> B) , (((((bigops.sameF_upto) (bool.bool)) (k)) (p1)) (p2)) -> ((((((bigops.sameF_p) (B)) (k)) (p1)) (f)) (g)) -> (((logic.eq_) (B)) (((((((bigops.bigop) (B)) (k)) (fun (i : nat.nat) , (p1) (i))) (nil)) (op)) (fun (i : nat.nat) , (f) (i)))) (((((((bigops.bigop) (B)) (k)) (fun (i : nat.nat) , (p2) (i))) (nil)) (op)) (fun (i : nat.nat) , (g) (i))).

same_bigop [B:TYPE+] : LEMMA (FORALL(k: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(nil:B):(FORALL(op:[B -> [B -> B]]):(FORALL(f:[nat_sttfa_th.sttfa_nat -> B]):(FORALL(g:[nat_sttfa_th.sttfa_nat -> B]):(bigops_sttfa.sameF_upto[bool_sttfa_th.sttfa_bool](k)(p1)(p2) => (bigops_sttfa.sameF_p[B](k)(p1)(f)(g) => logic_sttfa_th.eq[B](bigops_sttfa.bigop[B](k)((LAMBDA(i:nat_sttfa_th.sttfa_nat):p1(i)))(nil)(op)((LAMBDA(i:nat_sttfa_th.sttfa_nat):f(i))))(bigops_sttfa.bigop[B](k)((LAMBDA(i:nat_sttfa_th.sttfa_nat):p2(i)))(nil)(op)((LAMBDA(i:nat_sttfa_th.sttfa_nat):g(i)))))))))))))

Printing for OpenTheory is not working at the moment.