proposition: Lemma allC (B1 B2 : Type) (q : B1 -> B2 -> post A) : conseq s p (fun y i m => forall x1 x2, q x1 x2 y i m) <-> conseq s p (fun y i m => forall x, q x.1 x.2 y i m).
proof: Proof. split=>H1 i H2 D1; case: (H1 i H2 D1)=>S1 S2. - by split=>// y m H D [x1 x2]; apply: S2. by split=>// y m H D x1 x2; apply: (S2 y m H D (x1, x2)). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)