- ground_2: update ...

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / nstream_id.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma
index b80af74851ee0cfaff504d992eab4a91fdab8669..f5103e257aeef7cf8d432d309e118400ed48c6f1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma
@@ -149,7 +149,5 @@ qed-.
 lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≡ f →  𝐈⦃f2⦄ → f1 ≐ f.
 /3 width=8 by isid_after_dx, after_mono/
 qed-.
-(*
-lemma after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃t⦄ → 𝐈⦃t1⦄ ∧ 𝐈⦃t2⦄.
-qed-.
-*)
+
+axiom after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄ ∧ 𝐈⦃f2⦄.