proposition: Lemma noConf_HProp (x y : nat) : (forall p q : x = y, p = q).
proof: Proof. unshelve refine (apply_equiv_dom _ _ _). shelve. refine (equiv_sym (NoConfusionPackage_isequiv x y)). intros x0. unshelve refine (apply_equiv_dom _ _ _). shelve. refine (equiv_sym (NoConfusionPackage_isequiv x y)). revert x0. revert x y. fix 1. unfold equiv, equiv_inv, equiv_sym, inv_equiv, NoConfusionPackage_isequiv, NoConfusion.noConfusion_nat_obligation_1; simpl; unfold equiv, equiv_inv, equiv_sym, inv_equiv, NoConfusionPackage_isequiv, NoConfusion.noConfusion_nat_obligation_1; simpl. destruct x; destruct y; intros. destruct x0, x. reflexivity. destruct x0. destruct x0. change (Top.cong S x0 = Top.cong S x1). apply Top.cong. simpl in x0, x1. intros. simpl in x0, x1. pose (equiv (NoConfusionPackage_isequiv x y) x0). pose (equiv (NoConfusionPackage_isequiv x y) x1). specialize (noConf_HProp _ _ n n0). simpl. subst n n0. change ( @equiv (@NoConfusion nat NoConfusionPackage_nat x y) (@Logic.eq nat x y) (@equiv_sym (@Logic.eq nat x y) (@NoConfusion nat NoConfusionPackage_nat x y) (@NoConfusionPackage_isequiv nat x y NoConfusionPackage_nat))) with (@inv_equiv _ _ (@NoConfusionPackage_isequiv nat x y NoConfusionPackage_nat)) in *. rewrite equiv_inv_equiv in noConf_HProp. rewrite equiv_inv_equiv in noConf_HProp. apply noConf_HProp. Defined.
imports: Equations Utf8 DepElimDec EqDecInstances