proposition: Lemma noConfVec_eq_eq_inv {A n} (v v' : Vec A n) (e : v = v') : noConfVec_eq_inv _ _ (noConfVec_eq _ _ e) = e.
proof: Proof. destruct e. destruct v; reflexivity. Defined.
imports: Program Bvector List Relations Equations(Equations Signature DepElimDec) Utf8