{G : Group} (H K : Subgroup G) (P : forall x, subgroup_product H K x -> Type) (P_H_in : forall x y, P x (tr (sgt_in (inl y)))) (P_K_in : forall x y, P x (tr (sgt_in (inr y)))) (P_unit : P mon_unit (tr sgt_unit)) (P_op : forall x y h k, P x (tr h) -> P y (tr k) -> P (x * - y) (tr (sgt_op h k))) `{forall x y, IsHProp (P x y)} : forall x (p : subgroup_product H K x), P x p. Proof. intros x p. strip_truncations. induction p as [x s | | x y h IHh k IHk]. + destruct s. - apply P_H_in. - apply P_K_in. + exact P_unit. + by apply P_op. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.