- letin X ≝ (sig_in ?? x h);
- letin Xi ≝ (λn.sig_in ?? (xi n) (Hxi n));
- letin Yi ≝ (λn.sig_in ?? (yi n) (Hyi n));
- letin Ai ≝ (λn:nat.sig_in ?? (a n) (H1 n));
- apply (sandwich {[l,u]} X 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;