proposition: Lemma noconf_inv : forall (A : Type) (a b : &{ index : nat & vector A index}), NoConf A a b -> a = b.
proof: Proof. intros. destruct a, b. destruct pr2, pr3; try constructor || contradiction. simpl in H. NoConfusion.destruct_tele_eq H. reflexivity. Defined.
imports: Equations DepElimDec EqDecInstances