matita/matita/contribs/lambdadelta/basic_2/etc/lsubf.etc

   1 (* A Basic_A2 lemma we do not need so far *)
   2 lemma lsubf_sle_div: ∀f,f2,L1,L2. ⦃L1, f⦄ ⫃ 𝐅* ⦃L2, f2⦄ →
   3                      ∀f1. f1 ⊆ f2 → ⦃L1, f⦄ ⫃ 𝐅* ⦃L2, f1⦄.
   4 #f #f2 #L1 #L2 #H elim H -f -f2 -L1 -L2
   5 /4 width=3 by lsubf_beta, lsubf_bind, lsubf_atom, sle_tl, sle_trans/
   6 qed-.