proposition: Lemma big_ind3 I r (P : pred I) F1 F2 F3 (K_F : forall i, P i -> K (F1 i) (F2 i) (F3 i)) : K (\big[op1/id1]_(i <- r | P i) F1 i) (\big[op2/id2]_(i <- r | P i) F2 i) (\big[op3/id3]_(i <- r | P i) F3 i).
proof: Proof. by apply: big_rec3 => i x1 x2 x3 /K_F; apply: Kop. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)