proposition: Lemma noConfVec_eq_inv_eq {A n} (v v' : Vec A n) (e : noConfVec v v') : noConfVec_eq _ _ (noConfVec_eq_inv _ _ e) = e.
proof: Proof. destruct v; revert e; depelim v'; simplify *; reflexivity. Defined.
imports: Equations(Equations DepElimDec HSets) Utf8