fact: Definition square_tel {Δ : Tel} {w x y z : Δ} (t : w =={Δ} x) (b : y == z) (l : w == y) (r : x == z) : Tel := subst (fun x : Δ => x == y) t l =={fun y => x == y;b} r.
imports: Equations Utf8 DepElimDec EqDecInstances