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