Finish upgrading

theories/properties.v

@@ -211,7 +211,7 @@ Module Typing.
       hauto lq:on inv:Level.
   Qed.
 
-  Lemma upgrading Φ Γ Δ a ℓ A :
+  Lemma upgrading_liftable Φ Γ Δ a ℓ A :
     Γ ⊢ a ;; ℓ ∈ A ->
     liftable Φ a ->
     ctx_fleq Φ Γ Δ ->
@@ -236,4 +236,56 @@ Module Typing.
       simpl. by constructor.
   Qed.
 
+  Definition or_lvl (a : bool) l :=
+    match l with
+    | Fixed ℓ => Fixed ℓ
+    | Floating ℓ => Floating (a || ℓ)
+    end.
+
+  Definition or_ctx (a : bool) : ctx -> ctx := map (fun '(ℓ,A) => (or_lvl a ℓ, A)).
+
+  Lemma or_fixed_ctx ℓ (Γ : ctx) :
+    fixed_ctx (or_ctx ℓ Γ) = fixed_ctx Γ.
+  Proof.
+    elim : Γ => //=.
+    - case => //=.
+      move => ℓ0 _ Γ.
+      move => h0. f_equal => //.
+      destruct ℓ0 => //=.
+  Qed.
+
+  Definition or_ctx_lookup ℓ0 i Γ ℓ A :
+    lookup i Γ (ℓ, A) ->
+    lookup i (or_ctx ℓ0 Γ) (or_lvl ℓ0 ℓ, A).
+  Proof.
+    elim : Γ i ℓ A; sauto.
+  Qed.
+
+  Lemma upgrading Γ a ℓ A :
+    Γ ⊢ a ;; ℓ ∈ A ->
+    or_ctx ℓ Γ ⊢ a ;; ℓ ∈ A.
+  Proof.
+    move => h. elim : Γ a ℓ A /h.
+    - move => Γ ℓ i ℓ0 A hℓ hi.
+      move /(or_ctx_lookup ℓ) in hi.
+      apply T_Var with (ℓ0 := or_lvl ℓ ℓ0); eauto.
+      destruct ℓ0, ℓ => //=.
+    - hauto lq:on ctrs:Wt.
+    - move => Γ ℓ a A B /= ha iha.
+      rewrite Bool.orb_diag in iha.
+      hauto lq:on ctrs:Wt.
+    - move => Γ ℓ ℓ0 a b A B hb ihb ha iha hla.
+      econstructor; eauto.
+      + apply : upgrading_liftable. apply ha. eauto. clear.
+        elim : Γ => //=.
+        * constructor.
+        * case => //= ℓ0 A Γ h0.
+          destruct ℓ0 => //=.
+          by constructor.
+          constructor => //.
+          clear. sauto lq:on.
+      + by rewrite or_fixed_ctx.
+    - hauto lq:on ctrs:Wt.
+  Qed.
+
 End Typing.