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