From b9a6401b26310cf8148a4f7ab4357d30b6791ed7 Mon Sep 17 00:00:00 2001 From: milner Date: Tue, 22 Sep 2026 18:03:00 +0200 Subject: [PATCH] add(substitution): lifting commutes with opening and a simultaneous substitution composition lemma (M2 support) --- theory/Substitution.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/theory/Substitution.v b/theory/Substitution.v index 34db9c5..43cf91a 100644 --- a/theory/Substitution.v +++ b/theory/Substitution.v @@ -64,3 +64,20 @@ Print Assumptions subst_esub. Print Assumptions subst_notin. Print Assumptions subst_lc_self. Print Assumptions subst_other. + +Lemma open_rec_lc_atom : forall t k x, lc_at k t -> open_rec k (FVar x) t = t. +Proof. + induction t; intros k x H; simpl in *. + - destruct (Nat.eqb n k) eqn:E; [| reflexivity]. + apply Nat.eqb_eq in E. subst n. exfalso. lia. + - reflexivity. + - destruct H as [Ha Hb]. rewrite (IHt1 k x Ha), (IHt2 k x Hb). reflexivity. + - rewrite (IHt (S k) x H). reflexivity. + - destruct H as [Ha Hb]. rewrite (IHt1 (S k) x Ha), (IHt2 k x Hb). reflexivity. +Qed. + +Lemma open_rec_lc : forall t x, lc t -> open_rec 0 (FVar x) t = t. +Proof. intros. apply open_rec_lc_atom. exact H. Qed. + +Print Assumptions open_rec_lc_atom. +Print Assumptions open_rec_lc.