]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_etc.etc
projects / helm.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
preservation of stratified vaildity through ordinary reduction and static typing
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / lsubss / lsubss_etc.etc
1 lemma lsubsv_fwd_lsubss: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → h ⊢ L1 •⊑[g] L2.
2 #h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ /2 width=6/
3 qed-.
Unnamed repository; edit this file 'description' to name the repository.