proposition: Lemma in3_sig : {in D1 & D2 & D3, {all3 P3}} -> forall (x : sig D1) (y : sig D2) (z : sig D3), P3 (sval x) (sval y) (sval z).
proof: Proof. by move=> DP [x Dx] [y Dy] [z Dz]; have := DP _ _ _ Dx Dy Dz. Qed.
imports: ssreflect ssrfun