proposition: Lemma antiframe p q i m h : def (i :+ h) -> (p --o q) (i :+ h) (m :+ h) -> (p --o q) i m.
proof: Proof. move=>D1 H i2 m2 E D2 H1; rewrite {i}E in H D1 D2 *. move: (H i2 (m2 :+ h)); rewrite unA; case/(_ (erefl _) D1 H1)=>h2 [E][D3]. rewrite unA in E; exists h2; rewrite (unKhl D3 E). by rewrite E in D3; rewrite (defUnl D3). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)