proposition: Lemma sub_in21 T T3 d d' d3 d3' (P : T -> T -> T3 -> Prop) : sub_mem d d' -> sub_mem d3 d3' -> forall Ph : ph {all3 P}, prop_in21 d' d3' Ph -> prop_in21 d d3 Ph.
proof: Proof. by move=> /= sub sub3; apply: sub_in111. Qed.
imports: ssreflect ssrfun