proposition: Lemma in_on1lP : {in D1, {on D2, allQ1l f & h}} <-> {in [pred x in D1 | f x \in D2], allQ1l f h}.
proof: Proof. split => allf x; have := allf x; rewrite inE => Q1f; first by case/andP. by move=> ? ?; apply: Q1f; apply/andP. Qed.
imports: ssreflect ssrfun