proposition: Lemma subst_compatible_par s s' sigma sigma': s ≫ s' -> (forall x, sigma x ≫ sigma' x) -> (sigma • s) ≫ (sigma'• s').
proof: Proof. induction 1 in sigma, sigma' |-*; cbn; trivial. - intros; econstructor; eapply IHpar. intros []; cbn; eauto using ren_compatible_par. - intros; econstructor. eapply IHpar1 with (sigma' := up sigma'); auto. intros []; cbn; eauto using ren_compatible_par. eapply IHpar2; auto. subst; now asimpl. - auto. Qed.
imports: Morphisms Setoid Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms semantics)