proposition: Lemma comb_proc_red s : closed s -> proc s \/ exists t, s ≻ t.
proof: Proof. Proof with try tauto. intros cls_s. induction s. - eapply closed_dcl in cls_s. inv cls_s. lia. - eapply closed_app in cls_s. destruct IHs1 as [[C [t A]] | A], IHs2 as [[D [t' B]] | B]... + right. subst. eexists. eauto. + right; subst. firstorder; eexists. eapply stepAppR. eassumption. + right; subst. firstorder; eexists. eapply stepAppL. eassumption. + right. subst. firstorder. eexists. eapply stepAppR. eassumption. - left. split. eassumption. firstorder. Qed.
imports: Lia