proposition: Lemma noconf : forall (A : Type) (a b : &{ index : nat & vector A index}), a = b -> NoConf A a b.
proof: Proof. intros. destruct H. destruct a. simpl. destruct pr2. simpl. exact I. simpl. reflexivity. Defined.
imports: Equations DepElimDec EqDecInstances