proposition: Lemma sect@{i} : forall (Δ : Tel@{i}) (u v : Δ), Sect@{i i} (eq_eq_equiv_inv Δ u v) (eq_eq_equiv Δ u v).
proof: Proof. induction Δ. simpl. intros. intro. constructor. intros u v. intros He. simpl in * |-. Opaque path_sigma_uncurried path_sigma path_sigma_equivalence path_sigma_equiv. pose proof (eissect (path_sigma_uncurried u v)). simpl. red in H0. Transparent path_sigma_uncurried path_sigma path_sigma_equivalence path_sigma_equiv. match goal with |- context[equiv _ ?x] => set (foo:=x) end. specialize (H0 foo). set (bar := (equiv_inv@{i} (equiv@{i} _ foo))) in *. change (bar = foo) in H0. symmetry in H0. unfold foo in H0. subst foo. clearbody bar. revert bar H0. refine (@Top.subst2@{i i} _ _ _ _). simpl. simpl. red in H. specialize (H _ _ _ He.2). destruct He. simpl. apply Top.cong. apply H. Defined.
imports: Equations Utf8 DepElimDec