intros;
cases (POW_full (concr S) (concr T) (Oconcr_rel ?? f)) (gc Hgc);
cases (POW_full (form S) (form T) (Oform_rel ?? f)) (gf Hgf);
intros;
cases (POW_full (concr S) (concr T) (Oconcr_rel ?? f)) (gc Hgc);
cases (POW_full (form S) (form T) (Oform_rel ?? f)) (gf Hgf);