X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Flsubc_drops.ma;h=5685fd1ef9bcc7338d20dd1f80870a8b6c73634b;hb=795ac6cc4ef54b4470b5e2fba287acca440c9c18;hp=90a7aa04184f6924f316a3028db1732e25a484bc;hpb=abd0169d8025bf4d613a612231ad5b0c4c1db009;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma index 90a7aa041..5685fd1ef 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma @@ -20,7 +20,7 @@ include "basic_2/computation/lsubc_drop.ma". (* Basic_1: was: csubc_drop1_conf_rev *) lemma drops_lsubc_trans: ∀RR,RS,RP. - acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) → + acp RR RS RP → acr RR RS RP RP → ∀G,L1,K1,des. ⇩*[Ⓕ, des] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 → ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⇩*[Ⓕ, des] L2 ≡ K2. #RR #RS #RP #Hacp #Hacr #G #L1 #K1 #des #H elim H -L1 -K1 -des