proposition: Lemma refine_eq_left {A} {x y w : A} (e : y = x) (P : x = w -> Type) : (forall (H : y = w), P (e [fun x => x = w]# H)) -> (forall (H : x = w), P H).
proof: Proof. destruct e. simpl. exact id. Defined.
imports: Equations(Equations)