From afb5d82d388986bbeb17a4f114aebbaafc948f93 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 7 Aug 2022 19:37:11 +0200 Subject: [PATCH] update in ground + additions to nap and xap --- .../matita/contribs/lambdadelta/ground/relocation/nap.ma | 8 ++++++++ .../matita/contribs/lambdadelta/ground/relocation/xap.ma | 8 ++++++++ 2 files changed, 16 insertions(+) diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma index ac32304ed..a5ab2dcb7 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma @@ -1,5 +1,6 @@ include "ground/relocation/tr_uni_pap.ma". include "ground/relocation/tr_compose_pap.ma". +include "ground/relocation/tr_pap_eq.ma". include "ground/notation/functions/applysucc_2.ma". include "ground/arith/nat_lt.ma". include "ground/arith/nat_plus_rplus.ma". @@ -53,3 +54,10 @@ lemma tr_nap_pushs_lt (f) (n) (m): tr_pap_plus // qed. + +theorem tr_xap_eq_repl (i): + stream_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩). +#i #f1 #f2 #Hf +