- letin Xi ≝ (⌊n,mk_sigT ?? (xi n) (Hxi n)⌋);
- letin Yi ≝ (⌊n,mk_sigT ?? (yi n) (Hyi n)⌋);
- letin Ai ≝ (⌊n,mk_sigT ?? (a n) (H1 n)⌋);
- apply (sandwich {[l,u]} (mk_sigT ?? x h) Xi Yi Ai); try assumption;
+ letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋);
+ letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋);
+ letin Ai ≝ (⌊n,≪a n, H1 n≫⌋);
+ apply (sandwich {[l,u]} ≪?, h≫ Xi Yi Ai); try assumption;