(F G : I → Type) {ℓ : list I} (R : ∀ i, F i -> G i -> Type) : FamilyProd F ℓ → FamilyProd G ℓ → Type := match ℓ with | nil => λ _ _, Unit | i :: _ => λ '(x,s) '(y,t), R i x y ∧ F G R s t end.
Require Import