proposition: Lemma rew_sym@{i} (A : Type@{i}) {Δ : A -> Tel@{i}} (x y : A) (px : Δ x) (py : Δ y) (e : y = x) : px =={Δ x} Top.subst (P:=Δ) e py -> Top.subst (P:=Δ) (eq_sym e) px =={Δ y} py.
proof: Proof. destruct e. simpl. trivial. Defined.
imports: Equations Utf8 DepElimDec EqDecInstances