Bonak.νSet.RewLemmas

Import Logic.EqNotations.

Set Warnings "-notation-overridden".
From Bonak Require Import HSet Notation.

Lemma rew_permute_ll_hset: ∀ (A: Type) (P Q: A → HSet) (x y: A)
  (H: ∀ z: A, P z = Q z) (H': x = y) (a: P x),
  rew [Dom] H y in rew [P] H' in a = rew [Q] H' in rew [Dom] H x in a.
Proof.
  now destruct H'.
Defined.

Lemma rew_swap: ∀ A (P: A → Type) a b (H: a = b) (x: P a) (y: P b),
  x = rew <- H in y ↔ rew H in x = y.
Proof.
  now destruct H.
Qed.

Lemma rew_app_rl A (P: A → Type) (x y: A) (H H': x = y) (a: P x) :
  H = H' → rew <- [P] H in rew [P] H' in a = a.
Proof.
  intros × →. now destruct H'.
Qed.

Lemma map_subst_app {A B} {x y} {𝛉: A} (H: x = y :> B) (P: A → B → Type)
  (f: ∀ 𝛉, P 𝛉 x):
  rew [P 𝛉] H in f 𝛉 = (rew [fun x ⇒ ∀ 𝛉, P 𝛉 x] H in f) 𝛉.
Proof.
  now destruct H.
Qed.