proposition: Lemma copy_xH : forall x, R (copy 1 x) x.
proof: Proof. intros; unfold copy; rewrite Prect_base. reflexivity. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)