get_lem' {KT VT} Key {lem} `{@respects_equivalence_db KT VT Key lem} : VT := lem. Notation get_lem key := ltac:(let res := constr:(get_lem' key) in let res' := (eval unfold get_lem' in res) in exact res') (only parsing). Section const. Context {A : Type} {T : Type}. Global Instance const_respects_equivalenceL : RespectsEquivalenceL A (fun _ _ => T). Proof. refine (fun _ _ => equiv_idmap T; fun _ => _). exact idpath. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.Tactics. Require Import Types.Equiv Types.Prod Types.Forall Types.Sigma Types.Universe.