proposition: Lemma sub_in12 T1 T d1 d1' d d' (P : T1 -> T -> T -> Prop) : sub_mem d1 d1' -> sub_mem d d' -> forall Ph : ph {all3 P}, prop_in12 d1' d' Ph -> prop_in12 d1 d Ph.
proof: Proof. by move=> /= sub1 sub; apply: sub_in111. Qed.
imports: ssreflect ssrfun