proposition: Lemma eval_sequal: forall x y, sequal x y -> forall A B x', eval A B x x' -> exists2 y', eval A B y y' & x'==y'.
proof: Proof. intros x y H. cut ((forall A B x', eval A B x x' -> exists2 y', eval A B y y' & x'==y') /\ (forall A B y', eval A B y y' -> exists2 x', eval A B x x' & y'==x')); [tauto| ]. induction H; (apply and_idem || split); intros A B xe Hx; eval_inversion; split_IHeval; eauto with algebra; eauto using Graph.equal_trans. destruct (eval_type_inj_left H4 H5) as [HB | Hz]; [ destruct HB | rewrite Hz in H; discriminate ]. eexists; eauto. rewrite (eval_inj H4 H5); symmetry; apply dot_distr_left. destruct (eval_type_inj_right H2 H3) as [HB | Hz]; [ destruct HB | rewrite Hz in H; discriminate ]. eexists; eauto. rewrite (eval_inj H3 H2); symmetry; apply dot_distr_right. eexists; eauto. rewrite (eval_inj H0 H1); apply plus_idem. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)