proposition: Lemma subset_types_imp_guarded_rel_choice_iff_rel_choice : ProofIrrelevance -> (GuardedRelationalChoice <-> RelationalChoice).
proof: Proof. intuition auto using guarded_rel_choice_imp_rel_choice, rel_choice_and_proof_irrel_imp_guarded_rel_choice. Qed.
imports: RelationClasses Logic