proposition: Lemma pr2_pair : forall x y : E, pr2 (pair x y) = y.
proof: Proof. ir. set (u := pair x y) in *. assert (is_pair u). unfold u in |- *. ap pair_is_pair. pose (pair_recov H). unfold pair_recovers in (type of p). unfold u in (type of p). pose (lem2 p). am. Qed.
imports: tactics