proposition: Lemma replace_replace_neq A: forall n p1 p2 (v : t A n) a b, p1 <> p2 -> replace (replace v p1 a) p2 b = replace (replace v p2 b) p1 a.
proof: Proof. apply (Fin.rect2 (fun n p1 p2 => forall v a b, p1 <> p2 -> replace (replace v p1 a) p2 b = replace (replace v p2 b) p1 a)). - intros n v a b Hneq. now contradiction Hneq. - intros n p2 v; revert n v p2. refine (@rectS _ _ _ _); auto. - intros n p1 v; revert n v p1. refine (@rectS _ _ _ _); auto. - intros n p1 p2 IH v; revert n v p1 p2 IH. refine (@rectS _ _ _ _); simpl; intro n; [| do 3 intro]; intros ? ? IH p1 p2; intro Hneq; f_equal; apply IH; intros Heq; apply Hneq; now subst. Qed.
imports: VectorDef PeanoNat Eqdep_dec