proposition: Lemma noconf : forall (A : Type) (a b : &{ index : nat & vector A index}), a =={ext nat (fun n => inj (vector A n))} b -> NoConf A a b.
proof: Proof. intros. destruct X. destruct a, b, pr1, pr2. simpl. destruct pr3. simpl. simpl. exact tt. simpl. exists eq_refl. exists eq_refl. simpl. constructor. Defined.
imports: Equations DepElimDec EqDecInstances Utf8