include "models/q_support.ma".
include "models/list_support.ma".
include "logic/cprop_connectives.ma".
include "models/q_support.ma".
include "models/list_support.ma".
include "logic/cprop_connectives.ma".
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).