]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/etc/cpx/cpx_length.etc
projects / helm.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
- updated equivalence on referred entries: it nust be degree-based
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / cpx / cpx_length.etc
1 lemma cpx_inv_lref1_ge: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[h] T2 → |L| ≤ i → T2 = #i.
Unnamed repository; edit this file 'description' to name the repository.