proposition: Lemma copy_plus : forall n m x, R (copy (n+m) x) (plus (copy n x) (copy m x)).
proof: Proof. unfold copy. induction n using Pind; intros m x. rewrite Prect_base. rewrite <- Pplus_one_succ_l. rewrite Prect_succ. reflexivity. rewrite Pplus_succ_permute_l. rewrite 2Prect_succ. rewrite IHn. apply op. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)