proposition: Lemma noConfVec_eq_inv_eq_refl {A n} (v : Vec A n) : noConfVec_eq _ _ (noConfVec_eq_inv v v (noConfVec_refl v)) = (noConfVec_refl v).
proof: Proof. destruct v; reflexivity. Defined.
imports: Equations(Equations DepElimDec HSets) Utf8