proposition: Lemma lift_reflexivity {HR :Reflexive R}: forall x y, E x y -> R x y.
proof: Proof. destruct H. intros ? ? G. rewrite G. reflexivity. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)