include "apps_2/notation/models/upspoon_3.ma".

   al: nat → dd → dd;                      (* alignment *)

interpretation "alignment (model)"
   'UpSpoon M i d = (al M i d).

(* Note: lift: compatibility *)
   mf: compatible_3 … (al M) (eq …) (sq M) (sq M);
(* Note: lift: swap *)
   mw: ∀l1,l2,d. l2 ≤ l1 → ⫯[l2]⫯[l1]d ≗{M} ⫯[↑l1]⫯[l2]d;
(* Note: lift: sort evaluation *)
   mv: ∀l,s. ⫯[l](sv M s) ≗ sv M s;

theorem valign_swap (M): is_model M →
                         ∀l1,l2. l2 ≤ l1 →
                         ∀lv:evaluation ….  ⫯[l2]⫯[l1]lv ≗{M} ⫯[↑l1]⫯[l2]lv.
/2 width=1 by mw/ qed.

lemma valign_comp (M): is_model M →
                       ∀l. compatible_2 … (valign M l) (veq M) (veq M).
/2 width=1 by mf/ qed-.