proposition: Lemma subset_eq : forall A (P : A -> Prop) (n m : sig P), n = m <-> `n = `m.
proof: Proof. intros A P n m. destruct n as (x,p). destruct m as (x',p'). simpl. split ; intros H ; subst. - inversion H. reflexivity. - pi. Qed.
imports: Coq.Program.Utils Coq.Program.Equality ProofIrrelevance