proposition: Lemma J_refl {Δ : Tel} (r : Δ) (P : forall s : Δ, eq Δ r s -> Type) (p : P r (refl r)) : J r P p r (refl r) = p.
proof: Proof. induction Δ. simpl. reflexivity. simpl. destruct r. refine (H pr1 pr2 _ _). Defined.
imports: Equations Utf8 DepElimDec