proposition: Lemma reverse_dup p : reverse (dup p) = dup (reverse p).
proof: Proof. induction p as [p IH|p IH|]; simpl. - rewrite 3!reverse_xI. rewrite (assoc_L (++)). rewrite IH. rewrite dup_app. reflexivity. - rewrite 3!reverse_xO. rewrite (assoc_L (++)). rewrite IH. rewrite dup_app. reflexivity. - reflexivity. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)