proposition: Lemma noConf_fin_eq_eq_inv {n} (v v' : fin n) (e : v = v') : noConf_fin_eq_inv _ _ (noConf_fin_eq _ _ e) = e.
proof: Proof. destruct e. destruct v; reflexivity. Defined.
imports: Equations(Equations DepElimDec HSets) Utf8