proposition: Lemma noConfusion_nat_k3 (x : nat) (p : noConf_nat x x) : noConfusion_nat_k x x p = eq_refl.
proof: Proof. induction x. simpl. destruct p. reflexivity. simpl. rewrite IHx. reflexivity. Defined.
imports: Equations Utf8 DepElimDec EqDecInstances