proposition: Lemma noconf_inv : forall (A : Type) (a b : &{ index : nat & vector A index}), NoConf A a b -> a =={ext nat (fun n => inj (vector A n))} b.
proof: Proof. intros. destruct a, b. destruct pr2, pr3; try constructor || contradiction. simpl in X. exists eq_refl. constructor. unfold NoConf in X. cbv beta iota delta -[telescope eq_expl] in X. apply (@cong_tel (tele (x : A) (n : nat) in (vector A n)) (tele (n1 : nat) in vector A n1) (fun x => &(S x.2.1 & Vector.cons x.1 x.2.2)) _ _ X). Defined.
imports: Equations Utf8 DepElimDec EqDecInstances