From 36d2e3cd167b210e49bdbb1fba417f92ff73bd65 Mon Sep 17 00:00:00 2001 From: milner Date: Tue, 22 Sep 2026 16:40:00 +0200 Subject: [PATCH] add(metatheory): composition and context stability for nonempty reduction (M2 support) --- theory/Metatheory.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/theory/Metatheory.v b/theory/Metatheory.v index 22fc8b2..acadaf6 100644 --- a/theory/Metatheory.v +++ b/theory/Metatheory.v @@ -234,3 +234,17 @@ Print Assumptions red1_root_fv. Print Assumptions red1r_fv. Print Assumptions lemma_2_1_fv_preserved. Print Assumptions lemma_2_3_beta_sim. + +Lemma Plus_trans : forall R a b c, Plus R a b -> Plus R b c -> Plus R a c. +Proof. + intros R a b c H. + induction H as [a0 b0 HR | a0 b0 u0 HR HP IH]; intros Hbc. + - apply plusS with (u := b0). exact HR. exact Hbc. + - apply plusS with (u := b0). exact HR. apply IH. exact Hbc. +Qed. + +Lemma Plus_step_trans : forall R a b c, R a b -> Plus R b c -> Plus R a c. +Proof. intros. apply plusS with (u := b). exact H. exact H0. Qed. + +Print Assumptions Plus_trans. +Print Assumptions Plus_step_trans.