Require Import List.
From Undecidability.MinskyMachines
Require Import ndMM2.
Set Default Proof Using "Type".
Section ndMM2_monotonicity.
Variables loc : Set.
Notation "Σ // a ⊕ b ⊦ u" := (@ndmm2_accept loc Σ a b u) (at level 70, no associativity).
Infix "⊆" := incl (at level 70).
Tactic Notation "by" "constr" int(i) "with" hyp(H) := econstructor i; [ apply H | ]; eassumption.
Fact ndmm2_accept_mono Σ Θ a b u : Σ ⊆ Θ -> Σ // a ⊕ b ⊦ u -> Θ // a ⊕ b ⊦ u.
Proof.
intros H.
induction 1.
+ constructor; auto.
+ by constr 2 with H.
+ by constr 3 with H.
+ by constr 4 with H.
+ by constr 5 with H.
+ by constr 6 with H.
+ by constr 7 with H.
Qed.
End ndMM2_monotonicity.