λδ-2B is released

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / relocation / drops_drops.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma
index 0e57eb6aaa6e7f809f74f556340099bbca3d8440..f8a65c53638fd411f6c0506496939045416cfb4b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma
@@ -38,7 +38,7 @@ theorem drops_conf: ∀b1,f1,L1,L. ⇩*[b1,f1] L1 ≘ L →
 qed-.
 
 (* Basic_1: was: drop1_trans *)
-(* Basic_2A1: includes: drop_trans_ge drop_trans_le drop_trans_ge_comm 
+(* Basic_2A1: includes: drop_trans_ge drop_trans_le drop_trans_ge_comm
                         drops_drop_trans
 *)
 theorem drops_trans: ∀b1,f1,L1,L. ⇩*[b1,f1] L1 ≘ L →