definition llor: ynat → relation4 term lenv lenv lenv ≝ λd,T,L2,L1,L.
∧∧ |L1| = |L2| & |L1| = |L|
& (∀I1,I2,I,K1,K2,K,V1,V2,V,i.
definition llor: ynat → relation4 term lenv lenv lenv ≝ λd,T,L2,L1,L.
∧∧ |L1| = |L2| & |L1| = |L|
& (∀I1,I2,I,K1,K2,K,V1,V2,V,i.