X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsubstitution%2Flift_rmap_after.ma;h=e3dd359b087a311bc2ebbe8684754bcd97e3b3e6;hp=e209f97a70e39bdc926135c13fb78e5414e76a52;hb=7008128d354c6e998a87bc2febe9f86ea714869c;hpb=d06053844638d88936d711b66fddbcca2a9add1c diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_after.ma index e209f97a7..e3dd359b0 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_after.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_after.ma @@ -20,7 +20,7 @@ include "delayed_updating/substitution/lift_path.ma". (* Constructions with tr_after **********************************************) lemma lift_rmap_after (g) (f) (p:path): - ↑[↑[f]p]g∘↑[p]f = ↑[p](g∘f). + 🠢[g]🠡[f]p∘🠢[f]p = 🠢[g∘f]p. #g #f #p elim p -p // #l #p #IH