]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/apps_2/etc/models/model.etc
update in basic_2
[helm.git] / matita / matita / contribs / lambdadelta / apps_2 / etc / models / model.etc
1
2 lemma pippo: ∀M,v1,v2,d,i. [i⬐d] v1 ≐⦋M⦌ v2 → v1 ≐⦋M⦌ ↓[i,1] v2.
3 #M #v1 #v2 #d #i #H #j elim (lt_or_ge … j i) #Hij
4 [ >lower_lt // <(H j) >raise_lt //
5 | >lower_ge // <(H (j+1)) >raise_gt /2 width=1 by le_S_S/
6 ]
7 qed-.