proposition: Lemma impC (B : Type) (q1 q2 : heap -> B -> Prop) (r : B -> post A) : conseq s p (fun y i m => forall x, q1 i x -> q2 i x -> r x y i m) <-> conseq s p (fun y i m => forall x, q1 i x /\ q2 i x -> r x y i m).
proof: Proof. split=>H1 i H2 D1; case: (H1 i H2 D1)=>S1 S2. - by split=>// y m H D x []; apply: S2. by split=>// *; apply: S2. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)