- the trace is explicit in all auto tactics with depth > 1

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / lprs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma
index ddf4e24ca81b01c40fa695fe16d124e03414c501..4bc12d246b22890658eaf8f5c571c122ba1f7279 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma
@@ -43,16 +43,16 @@ qed-.
 (* Basic properties *********************************************************)
 
 lemma lpr_lprs: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡* L2.
-/2 width=1/ qed.
+/2 width=1 by inj/ qed.
 
 lemma lprs_refl: ∀G,L. ⦃G, L⦄ ⊢ ➡* L.
-/2 width=1/ qed.
+/2 width=1 by lpr_lprs/ qed.
 
 lemma lprs_strap1: ∀G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡* L → ⦃G, L⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡* L2.
-/2 width=3/ qed.
+/2 width=3 by step/ qed-.
 
 lemma lprs_strap2: ∀G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡ L → ⦃G, L⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡* L2.
-/2 width=3/ qed.
+/2 width=3 by TC_strap/ qed-.
 
 lemma lprs_pair_refl: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡* L2.ⓑ{I}V.
 /2 width=1 by TC_lpx_sn_pair_refl/ qed.