proposition: Lemma reflexive_for_all_2_family_prod (F : I → Type) (R : ∀ i, Relation (F i)) `{!∀ i, Reflexive (R i)} {ℓ : list I} (s : FamilyProd F ℓ) : for_all_2_family_prod F F R s s.
proof: Proof. Proof with try reflexivity. induction ℓ... split... apply IHℓ. Defined.
imports: HoTT.Utf8Minimal HoTT.Basics.Overture Types.Unit HoTT.Classes.implementations.list