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