X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Fnstream_after.ma;h=25bb3c60b8d832f50eae97d178fb93c7183099a8;hb=384b04944ac31922ee41418b106b8e19a19ba9f0;hp=f8b71a6a5b083d8bbe79a92e8dccbc99113e649a;hpb=83cf6c88d2d0bd2c8af86ab7f95bf94c1ae59bc9;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
index f8b71a6a5..25bb3c60b 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
@@ -129,6 +129,9 @@ lemma after_inv_const: ∀f1,f2,f,n2,n. n@f1 ⊚ n2@f2 ≡ n@f → f1 ⊚ f2 ≡
 ]
 qed-.
 
+lemma after_inv_total: ∀f1,f2,f. f1 ⊚ f2 ≡ f → f1 ∘ f2 ≗ f.
+/2 width=4 by after_mono/ qed-.
+
 (* Specific forward lemmas **************************************************)
 
 lemma after_fwd_hd: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f → f1@❴n2❵ = n.