- advances on free variables allow to reduce lleq_lpx_trans to llor_total :)

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / multiple / llor_ldrop.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_ldrop.ma
index d8a4789b0ce7e6b71cc2e141d15d2320b6304d2e..b766269e7ded295a859dd85500d3f722224ae256 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_ldrop.ma
@@ -19,4 +19,4 @@ include "basic_2/multiple/llor.ma".
 
 (* Advanced properties ******************************************************)
 
-axiom llor_total: ∀L1,L2,T. |L1| ≤ |L2| → ∃L. L1 ⩖[T] L2 ≡ L.
+axiom llor_total: ∀L1,L2,T,d. |L1| ≤ |L2| → ∃L. L1 ⩖[T, d] L2 ≡ L.