lemma q2_trans : ∀a,b,c:bar. a < b → b < c → a < c.
intros 3; cases a; cases b; cases c; unfold q2_lt; simplify; intros;
lemma q2_trans : ∀a,b,c:bar. a < b → b < c → a < c.
intros 3; cases a; cases b; cases c; unfold q2_lt; simplify; intros;
definition nth_base ≝ λf,n. \fst (\nth f ▭ n).
definition nth_height ≝ λf,n. \snd (\nth f ▭ n).
definition nth_base ≝ λf,n. \fst (\nth f ▭ n).
definition nth_height ≝ λf,n. \snd (\nth f ▭ n).