proposition: Lemma sub_narrowing : forall Q E F Z P S T, sub E P Q -> sub (F ++ Z ~ bind_sub Q ++ E) S T -> sub (F ++ Z ~ bind_sub P ++ E) S T.
proof: Proof. intros. eapply sub_narrowing_aux; eauto. apply sub_transitivity. Qed.
imports: Fsub.Fsub_LetSum_Lemmas