partial commit in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / lprs_aaa.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_aaa.ma
new file mode 100644 (file)
index 0000000..f88fb32
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_aaa.ma
@@ -0,0 +1,3 @@
+lemma lprs_aaa_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
+                     ∀L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+/3 width=5 by lprs_lpxs, lpxs_aaa_conf/ qed-.