Covering for free contexts

In Ctx/Ctx.v we have instanciated the relevant part of the abstract interface for concrete contexts. Here we tackle the rest of the structure. Basically, we need to provide case-splitting for deciding if a variable i : (Γ +▶ Δ) ∋ x is in Γ or in Δ. We could do this directly but we prove a slight generalization, going through the definition of coverings, a ternary relationship on concrete contexts witnessing that a context is covered by the two others (respecting order).

A covering

This inductive family provides proofs that some context zs is obtained by "zipping" together two other contexts xs and ys.

  Inductive cover : ctx X -> ctx X -> ctx X -> Type :=
  | CNil : ∅ₓ ⊎ ∅ₓ  ≡ ∅ₓ
  | CLeft  {x xs ys zs} : xs ⊎ ys ≡ zs -> (xs ▶ₓ x) ⊎ ys ≡ (zs ▶ₓ x)
  | CRight {x xs ys zs} : xs ⊎ ys ≡ zs -> xs ⊎ (ys ▶ₓ x) ≡ (zs ▶ₓ x)
  where "a ⊎ b ≡ c" := (cover a b c).

Basic useful coverings.

  Equations cover_nil_r xs : xs ⊎ ∅ₓ ≡ xs :=
    cover_nil_r ∅ₓ        := CNil ;
    cover_nil_r (xs ▶ₓ _) := CLeft (cover_nil_r xs) .
  #[global] Arguments cover_nil_r {xs}.

  Equations cover_nil_l xs : ∅ₓ ⊎ xs ≡ xs :=
    cover_nil_l ∅ₓ        := CNil ;
    cover_nil_l (xs ▶ₓ _) := CRight (cover_nil_l xs) .
  #[global] Arguments cover_nil_l {xs}.

This is the crucial one: the concatenation is covered by its two components.

  Equations cover_cat {xs} ys : xs ⊎ ys ≡ (xs +▶ ys) :=
    cover_cat ∅ₓ        := cover_nil_r ;
    cover_cat (ys ▶ₓ _) := CRight (cover_cat ys) .
  #[global] Arguments cover_cat {xs ys}.

A covering gives us two injective renamings, left embedding and right embedding.

  Equations r_cover_l {xs ys zs} : xs ⊎ ys ≡ zs -> xs ⊆ zs :=
    r_cover_l (CLeft c)  _ top     := top ;
    r_cover_l (CLeft c)  _ (pop i) := pop (r_cover_l c _ i) ;
    r_cover_l (CRight c) _ i       := pop (r_cover_l c _ i) .

  Equations r_cover_r {xs ys zs} : xs ⊎ ys ≡ zs -> ys ⊆ zs :=
    r_cover_r (CLeft c)  _ i       := pop (r_cover_r c _ i) ;
    r_cover_r (CRight c) _ top     := top ;
    r_cover_r (CRight c) _ (pop i) := pop (r_cover_r c _ i) .

Injectivity.

  Lemma r_cover_l_inj {xs ys zs} (p : xs ⊎ ys ≡ zs) [x] (i j : xs ∋ x)
    (H : r_cover_l p _ i = r_cover_l p _ j) : i = j .X: Type
F: Fam₁ X (ctx X)
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
x: X
i, j: xs ∋ x
H: r_cover_l p x i = r_cover_l p x j
i = j
  Proof.X: Type
F: Fam₁ X (ctx X)
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
x: X
i, j: xs ∋ x
H: r_cover_l p x i = r_cover_l p x j
i = j
    induction p.X: Type
F: Fam₁ X (ctx X)
x: X
i, j: ∅ₓ ∋ x
H: r_cover_l CNil x i = r_cover_l CNil x j
i = j
X: Type
F: Fam₁ X (ctx X)
x0: X
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
x: X
i, j: xs ▶ₓ x0 ∋ x
H: r_cover_l (CLeft p) x i = r_cover_l (CLeft p) x j
IHp: forall i j : xs ∋ x, r_cover_l p x i = r_cover_l p x j -> i = j
i = j
X: Type
F: Fam₁ X (ctx X)
x0: X
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
x: X
i, j: xs ∋ x
H: r_cover_l (CRight p) x i =
r_cover_l (CRight p) x j
IHp: forall i j : xs ∋ x, r_cover_l p x i = r_cover_l p x j -> i = j
i = j
    -X: Type
F: Fam₁ X (ctx X)
x: X
i, j: ∅ₓ ∋ x
H: r_cover_l CNil x i = r_cover_l CNil x j
i = j dependent elimination i.
    -X: Type
F: Fam₁ X (ctx X)
x0: X
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
x: X
i, j: xs ▶ₓ x0 ∋ x
H: r_cover_l (CLeft p) x i = r_cover_l (CLeft p) x j
IHp: forall i j : xs ∋ x, r_cover_l p x i = r_cover_l p x j -> i = j
i = j dependent elimination i; dependent elimination j; try now inversion H.X: Type
F: Fam₁ X (ctx X)
y0: X
Γ1, ys, zs: ctx X
p: Γ1 ⊎ ys ≡ zs
x: X
v, v0: var x Γ1
H: r_cover_l (CLeft p) x (pop v) =
r_cover_l (CLeft p) x (pop v0)
IHp: forall i j : Γ1 ∋ x, r_cover_l p x i = r_cover_l p x j -> i = j
pop v = pop v0
      apply noConfusion_inv in H.X: Type
F: Fam₁ X (ctx X)
y0: X
Γ1, ys, zs: ctx X
p: Γ1 ⊎ ys ≡ zs
x: X
v, v0: var x Γ1
H: NoConfusion (r_cover_l (CLeft p) x (pop v))
  (r_cover_l (CLeft p) x (pop v0))
IHp: forall i j : Γ1 ∋ x, r_cover_l p x i = r_cover_l p x j -> i = j
pop v = pop v0
      f_equal; now apply IHp.
    -X: Type
F: Fam₁ X (ctx X)
x0: X
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
x: X
i, j: xs ∋ x
H: r_cover_l (CRight p) x i =
r_cover_l (CRight p) x j
IHp: forall i j : xs ∋ x, r_cover_l p x i = r_cover_l p x j -> i = j
i = j apply noConfusion_inv in H.X: Type
F: Fam₁ X (ctx X)
x0: X
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
x: X
i, j: xs ∋ x
H: NoConfusion (r_cover_l (CRight p) x i)
  (r_cover_l (CRight p) x j)
IHp: forall i j : xs ∋ x, r_cover_l p x i = r_cover_l p x j -> i = j
i = j
      now apply IHp.
  Qed.

  Lemma r_cover_r_inj {xs ys zs} (p : xs ⊎ ys ≡ zs) [y] (i j : ys ∋ y)
    (H : r_cover_r p _ i = r_cover_r p _ j) : i = j .X: Type
F: Fam₁ X (ctx X)
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
y: X
i, j: ys ∋ y
H: r_cover_r p y i = r_cover_r p y j
i = j
  Proof.X: Type
F: Fam₁ X (ctx X)
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
y: X
i, j: ys ∋ y
H: r_cover_r p y i = r_cover_r p y j
i = j
    induction p.X: Type
F: Fam₁ X (ctx X)
y: X
i, j: ∅ₓ ∋ y
H: r_cover_r CNil y i = r_cover_r CNil y j
i = j
X: Type
F: Fam₁ X (ctx X)
x: X
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
y: X
i, j: ys ∋ y
H: r_cover_r (CLeft p) y i = r_cover_r (CLeft p) y j
IHp: forall i j : ys ∋ y, r_cover_r p y i = r_cover_r p y j -> i = j
i = j
X: Type
F: Fam₁ X (ctx X)
x: X
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
y: X
i, j: ys ▶ₓ x ∋ y
H: r_cover_r (CRight p) y i =
r_cover_r (CRight p) y j
IHp: forall i j : ys ∋ y, r_cover_r p y i = r_cover_r p y j -> i = j
i = j
    -X: Type
F: Fam₁ X (ctx X)
y: X
i, j: ∅ₓ ∋ y
H: r_cover_r CNil y i = r_cover_r CNil y j
i = j dependent elimination i.
    -X: Type
F: Fam₁ X (ctx X)
x: X
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
y: X
i, j: ys ∋ y
H: r_cover_r (CLeft p) y i = r_cover_r (CLeft p) y j
IHp: forall i j : ys ∋ y, r_cover_r p y i = r_cover_r p y j -> i = j
i = j apply noConfusion_inv in H; now apply IHp.
    -X: Type
F: Fam₁ X (ctx X)
x: X
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
y: X
i, j: ys ▶ₓ x ∋ y
H: r_cover_r (CRight p) y i =
r_cover_r (CRight p) y j
IHp: forall i j : ys ∋ y, r_cover_r p y i = r_cover_r p y j -> i = j
i = j dependent elimination i; dependent elimination j; try now inversion H.X: Type
F: Fam₁ X (ctx X)
y1: X
xs, Γ1, zs: ctx X
p: xs ⊎ Γ1 ≡ zs
y: X
v, v0: var y Γ1
H: r_cover_r (CRight p) y (pop v) =
r_cover_r (CRight p) y (pop v0)
IHp: forall i j : Γ1 ∋ y, r_cover_r p y i = r_cover_r p y j -> i = j
pop v = pop v0
      apply noConfusion_inv in H.X: Type
F: Fam₁ X (ctx X)
y1: X
xs, Γ1, zs: ctx X
p: xs ⊎ Γ1 ≡ zs
y: X
v, v0: var y Γ1
H: NoConfusion (r_cover_r (CRight p) y (pop v))
  (r_cover_r (CRight p) y (pop v0))
IHp: forall i j : Γ1 ∋ y, r_cover_r p y i = r_cover_r p y j -> i = j
pop v = pop v0
      f_equal; now apply IHp.
  Qed.

The two embeddings have disjoint images.

  Lemma r_cover_disj {xs ys zs} (p : xs ⊎ ys ≡ zs) [a] (i : xs ∋ a) (j : ys ∋ a)
    (H : r_cover_l p _ i = r_cover_r p _ j) : T0.X: Type
F: Fam₁ X (ctx X)
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
a: X
i: xs ∋ a
j: ys ∋ a
H: r_cover_l p a i = r_cover_r p a j
T0
  Proof.X: Type
F: Fam₁ X (ctx X)
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
a: X
i: xs ∋ a
j: ys ∋ a
H: r_cover_l p a i = r_cover_r p a j
T0
    induction p.X: Type
F: Fam₁ X (ctx X)
a: X
i, j: ∅ₓ ∋ a
H: r_cover_l CNil a i = r_cover_r CNil a j
T0
X: Type
F: Fam₁ X (ctx X)
x: X
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
a: X
i: xs ▶ₓ x ∋ a
j: ys ∋ a
H: r_cover_l (CLeft p) a i = r_cover_r (CLeft p) a j
IHp: forall (i : xs ∋ a) (j : ys ∋ a), ¬ (r_cover_l p a i = r_cover_r p a j)
T0
X: Type
F: Fam₁ X (ctx X)
x: X
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
a: X
i: xs ∋ a
j: ys ▶ₓ x ∋ a
H: r_cover_l (CRight p) a i =
r_cover_r (CRight p) a j
IHp: forall (i : xs ∋ a) (j : ys ∋ a), ¬ (r_cover_l p a i = r_cover_r p a j)
T0
    -X: Type
F: Fam₁ X (ctx X)
a: X
i, j: ∅ₓ ∋ a
H: r_cover_l CNil a i = r_cover_r CNil a j
T0 inversion i.
    -X: Type
F: Fam₁ X (ctx X)
x: X
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
a: X
i: xs ▶ₓ x ∋ a
j: ys ∋ a
H: r_cover_l (CLeft p) a i = r_cover_r (CLeft p) a j
IHp: forall (i : xs ∋ a) (j : ys ∋ a), ¬ (r_cover_l p a i = r_cover_r p a j)
T0 dependent elimination i.X: Type
F: Fam₁ X (ctx X)
a: X
Γ, ys, zs: ctx X
p: Γ ⊎ ys ≡ zs
j: ys ∋ a
H: r_cover_l (CLeft p) a top =
r_cover_r (CLeft p) a j
IHp: forall (i : Γ ∋ a) (j : ys ∋ a), ¬ (r_cover_l p a i = r_cover_r p a j)
T0
X: Type
F: Fam₁ X (ctx X)
y: X
Γ0, ys, zs: ctx X
p: Γ0 ⊎ ys ≡ zs
a: X
v: var a Γ0
j: ys ∋ a
H: r_cover_l (CLeft p) a (pop v) =
r_cover_r (CLeft p) a j
IHp: forall (i : Γ0 ∋ a) (j : ys ∋ a), ¬ (r_cover_l p a i = r_cover_r p a j)
T0
      +X: Type
F: Fam₁ X (ctx X)
a: X
Γ, ys, zs: ctx X
p: Γ ⊎ ys ≡ zs
j: ys ∋ a
H: r_cover_l (CLeft p) a top =
r_cover_r (CLeft p) a j
IHp: forall (i : Γ ∋ a) (j : ys ∋ a), ¬ (r_cover_l p a i = r_cover_r p a j)
T0 inversion H.
      +X: Type
F: Fam₁ X (ctx X)
y: X
Γ0, ys, zs: ctx X
p: Γ0 ⊎ ys ≡ zs
a: X
v: var a Γ0
j: ys ∋ a
H: r_cover_l (CLeft p) a (pop v) =
r_cover_r (CLeft p) a j
IHp: forall (i : Γ0 ∋ a) (j : ys ∋ a), ¬ (r_cover_l p a i = r_cover_r p a j)
T0 apply noConfusion_inv in H; cbn in H.X: Type
F: Fam₁ X (ctx X)
y: X
Γ0, ys, zs: ctx X
p: Γ0 ⊎ ys ≡ zs
a: X
v: var a Γ0
j: ys ∋ a
H: r_cover_l p a v = r_cover_r p a j
IHp: forall (i : Γ0 ∋ a) (j : ys ∋ a), ¬ (r_cover_l p a i = r_cover_r p a j)
T0
        exact (IHp v j H).
    -X: Type
F: Fam₁ X (ctx X)
x: X
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
a: X
i: xs ∋ a
j: ys ▶ₓ x ∋ a
H: r_cover_l (CRight p) a i =
r_cover_r (CRight p) a j
IHp: forall (i : xs ∋ a) (j : ys ∋ a), ¬ (r_cover_l p a i = r_cover_r p a j)
T0 dependent elimination j.X: Type
F: Fam₁ X (ctx X)
a: X
xs, Γ, zs: ctx X
p: xs ⊎ Γ ≡ zs
i: xs ∋ a
H: r_cover_l (CRight p) a i =
r_cover_r (CRight p) a top
IHp: forall (i : xs ∋ a) (j : Γ ∋ a), ¬ (r_cover_l p a i = r_cover_r p a j)
T0
X: Type
F: Fam₁ X (ctx X)
y: X
xs, Γ0, zs: ctx X
p: xs ⊎ Γ0 ≡ zs
a: X
i: xs ∋ a
v: var a Γ0
H: r_cover_l (CRight p) a i =
r_cover_r (CRight p) a (pop v)
IHp: forall (i : xs ∋ a) (j : Γ0 ∋ a), ¬ (r_cover_l p a i = r_cover_r p a j)
T0
      +X: Type
F: Fam₁ X (ctx X)
a: X
xs, Γ, zs: ctx X
p: xs ⊎ Γ ≡ zs
i: xs ∋ a
H: r_cover_l (CRight p) a i =
r_cover_r (CRight p) a top
IHp: forall (i : xs ∋ a) (j : Γ ∋ a), ¬ (r_cover_l p a i = r_cover_r p a j)
T0 inversion H.
      +X: Type
F: Fam₁ X (ctx X)
y: X
xs, Γ0, zs: ctx X
p: xs ⊎ Γ0 ≡ zs
a: X
i: xs ∋ a
v: var a Γ0
H: r_cover_l (CRight p) a i =
r_cover_r (CRight p) a (pop v)
IHp: forall (i : xs ∋ a) (j : Γ0 ∋ a), ¬ (r_cover_l p a i = r_cover_r p a j)
T0 apply noConfusion_inv in H; cbn in H.X: Type
F: Fam₁ X (ctx X)
y: X
xs, Γ0, zs: ctx X
p: xs ⊎ Γ0 ≡ zs
a: X
i: xs ∋ a
v: var a Γ0
H: r_cover_l p a i = r_cover_r p a v
IHp: forall (i : xs ∋ a) (j : Γ0 ∋ a), ¬ (r_cover_l p a i = r_cover_r p a j)
T0
        exact (IHp i v H).
  Qed.

Now we can start proving that the copairing of the two embeddings has non-empty fibers, ie, we can case split.

  Variant cover_view {xs ys zs} (p : xs ⊎ ys ≡ zs) [z] : zs ∋ z -> Type :=
  | Vcov_l  (i : xs ∋ z) : cover_view p (r_cover_l p _ i)
  | Vcov_r (j : ys ∋ z) : cover_view p (r_cover_r p _ j)
  .
  #[global] Arguments Vcov_l {xs ys zs p z}.
  #[global] Arguments Vcov_r {xs ys zs p z}.

Indeed!

  Lemma view_cover {xs ys zs} (p : xs ⊎ ys ≡ zs) [z] (i : zs ∋ z) : cover_view p i.X: Type
F: Fam₁ X (ctx X)
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
z: X
i: zs ∋ z
cover_view p i
  Proof.X: Type
F: Fam₁ X (ctx X)
xs, ys, zs: ctx X
p: xs ⊎ ys ≡ zs
z: X
i: zs ∋ z
cover_view p i
    revert xs ys p; induction zs; intros xs ys p; dependent elimination i.X: Type
F: Fam₁ X (ctx X)
Γ: ctx X
z: X
IHzs: forall (i : Γ ∋ z) (xs ys : ctx X)
  (p : xs ⊎ ys ≡ Γ), cover_view p i
xs, ys: ctx X
p: xs ⊎ ys ≡ (Γ ▶ₓ z)
cover_view p top
X: Type
F: Fam₁ X (ctx X)
Γ0: ctx X
y, z: X
v: var z Γ0
IHzs: forall (i : Γ0 ∋ z) (xs ys : ctx X)
  (p : xs ⊎ ys ≡ Γ0), cover_view p i
xs, ys: ctx X
p: xs ⊎ ys ≡ (Γ0 ▶ₓ y)
cover_view p (pop v)
    +X: Type
F: Fam₁ X (ctx X)
Γ: ctx X
z: X
IHzs: forall (i : Γ ∋ z) (xs ys : ctx X)
  (p : xs ⊎ ys ≡ Γ), cover_view p i
xs, ys: ctx X
p: xs ⊎ ys ≡ (Γ ▶ₓ z)
cover_view p top dependent elimination p; [ exact (Vcov_l top) | exact (Vcov_r top) ].
    +X: Type
F: Fam₁ X (ctx X)
Γ0: ctx X
y, z: X
v: var z Γ0
IHzs: forall (i : Γ0 ∋ z) (xs ys : ctx X)
  (p : xs ⊎ ys ≡ Γ0), cover_view p i
xs, ys: ctx X
p: xs ⊎ ys ≡ (Γ0 ▶ₓ y)
cover_view p (pop v) dependent elimination p.X: Type
F: Fam₁ X (ctx X)
zs: ctx X
x, z: X
v: var z zs
IHzs: forall (i : zs ∋ z) (xs ys : ctx X)
  (p : xs ⊎ ys ≡ zs), cover_view p i
xs0, ys0: ctx X
c: xs0 ⊎ ys0 ≡ zs
cover_view (CLeft c) (pop v)
X: Type
F: Fam₁ X (ctx X)
zs0: ctx X
x0, z: X
v: var z zs0
IHzs: forall (i : zs0 ∋ z) (xs ys : ctx X)
  (p : xs ⊎ ys ≡ zs0), cover_view p i
xs1, ys1: ctx X
c0: xs1 ⊎ ys1 ≡ zs0
cover_view (CRight c0) (pop v)
      *X: Type
F: Fam₁ X (ctx X)
zs: ctx X
x, z: X
v: var z zs
IHzs: forall (i : zs ∋ z) (xs ys : ctx X)
  (p : xs ⊎ ys ≡ zs), cover_view p i
xs0, ys0: ctx X
c: xs0 ⊎ ys0 ≡ zs
cover_view (CLeft c) (pop v) destruct (IHzs v _ _ c); [ exact (Vcov_l (pop i)) | exact (Vcov_r j) ].
      *X: Type
F: Fam₁ X (ctx X)
zs0: ctx X
x0, z: X
v: var z zs0
IHzs: forall (i : zs0 ∋ z) (xs ys : ctx X)
  (p : xs ⊎ ys ≡ zs0), cover_view p i
xs1, ys1: ctx X
c0: xs1 ⊎ ys1 ≡ zs0
cover_view (CRight c0) (pop v) destruct (IHzs v _ _ c0); [ exact (Vcov_l i) | exact (Vcov_r (pop j)) ].
  Qed.

Finishing the instanciation of the abstract interface for ctx X.

  #[global] Instance free_context_cat_wkn : context_cat_wkn X (ctx X) :=
    {| r_cat_l _ _ := r_cover_l cover_cat ;
       r_cat_r _ _ := r_cover_r cover_cat |}.

  #[global] Program Instance free_context_laws : context_laws X (ctx X).
  Next Obligation.X: Type
F: Fam₁ X (ctx X)
t: X
i: cvar ∅ₓ t
c_emp_view t i dependent elimination i. Qed.
  Next Obligation.X: Type
F: Fam₁ X (ctx X)
Γ, Δ: ctx X
t: X
i: cvar (ccat Γ Δ) t
c_cat_view Γ Δ t i
    destruct (view_cover cover_cat i).X: Type
F: Fam₁ X (ctx X)
Γ, Δ: ctx X
t: X
i: Γ ∋ t
c_cat_view Γ Δ t (r_cover_l cover_cat t i)
X: Type
F: Fam₁ X (ctx X)
Γ, Δ: ctx X
t: X
j: Δ ∋ t
c_cat_view Γ Δ t (r_cover_r cover_cat t j)
    now refine (Vcat_l _).X: Type
F: Fam₁ X (ctx X)
Γ, Δ: ctx X
t: X
j: Δ ∋ t
c_cat_view Γ Δ t (r_cover_r cover_cat t j)
    now refine (Vcat_r _).
  Qed.
  Next Obligation.X: Type
F: Fam₁ X (ctx X)
Γ, Δ: ctx X
t: X
injective (r_cover_l cover_cat t) intros ?? H; now apply r_cover_l_inj in H. Qed.
  Next Obligation.X: Type
F: Fam₁ X (ctx X)
Γ, Δ: ctx X
t: X
injective (r_cover_r cover_cat t) intros ?? H; now apply r_cover_r_inj in H. Qed.
  Next Obligation.X: Type
F: Fam₁ X (ctx X)
Γ, Δ: ctx X
t: X
i: cvar Γ t
j: cvar Δ t
H: r_cover_l cover_cat t i = r_cover_r cover_cat t j
T0 now apply r_cover_disj in H. Qed.

Additional utilities.

  Definition a_cover {Γ1 Γ2 Γ3 Δ} (p : Γ1 ⊎ Γ2 ≡ Γ3) (u : Γ1 =[F]> Δ) (v : Γ2 =[F]> Δ)
    : Γ3 =[F]> Δ
    := fun _ i => match view_cover p i with
               | Vcov_l i  => u _ i
               | Vcov_r j => v _ j
               end .
  #[global] Arguments a_cover _ _ _ _ _ _ _ _ /.

  #[global] Instance a_cover_proper {Γ1 Γ2 Γ3 Δ H}
    : Proper (asgn_eq _ _ ==> asgn_eq _ _ ==> asgn_eq _ _) (@a_cover Γ1 Γ2 Γ3 Δ H).X: Type
F: Fam₁ X (ctx X)
Γ1, Γ2, Γ3, Δ: ctx X
H: Γ1 ⊎ Γ2 ≡ Γ3
Proper
  (asgn_eq Γ1 Δ ==> asgn_eq Γ2 Δ ==> asgn_eq Γ3 Δ)
  (a_cover H)
  Proof.X: Type
F: Fam₁ X (ctx X)
Γ1, Γ2, Γ3, Δ: ctx X
H: Γ1 ⊎ Γ2 ≡ Γ3
Proper
  (asgn_eq Γ1 Δ ==> asgn_eq Γ2 Δ ==> asgn_eq Γ3 Δ)
  (a_cover H)
    intros ? ? H1 ? ? H2 ? i; unfold a_cover.X: Type
F: Fam₁ X (ctx X)
Γ1, Γ2, Γ3, Δ: ctx X
H: Γ1 ⊎ Γ2 ≡ Γ3
x, y: Γ1 =[ F ]> Δ
H1: x ≡ₐ y
x0, y0: Γ2 =[ F ]> Δ
H2: x0 ≡ₐ y0
a: X
i: Γ3 ∋ a
match view_cover H i with
| Vcov_l i => x a i
| Vcov_r j => x0 a j
end =
match view_cover H i with
| Vcov_l i => y a i
| Vcov_r j => y0 a j
end
    destruct (view_cover H i); [ now apply H1 | now apply H2 ].
  Qed.
End with_param.

#[global] Notation "a ⊎ b ≡ c" := (cover a b c).
#[global] Notation "a ▶ₐ v" := (a_append a v) : asgn_scope.
#[global] Notation "[ u , H , v ]" := (a_cover H u v) : asgn_scope.