include "basics/pts.ma".
-definition hint_declaration_Type0 ≝ λA:Type[0] .λa,b:A.Prop.
-definition hint_declaration_Type1 ≝ λA:Type[1].λa,b:A.Prop.
-definition hint_declaration_Type2 ≝ λa,b:Type[2].Prop.
-definition hint_declaration_CProp0 ≝ λA:CProp[0].λa,b:A.Prop.
-definition hint_declaration_CProp1 ≝ λA:CProp[1].λa,b:A.Prop.
-definition hint_declaration_CProp2 ≝ λa,b:CProp[2].Prop.
+\ 5img class="anchor" src="icons/tick.png" id="hint_declaration_Type0"\ 6definition hint_declaration_Type0 ≝ λA:Type[0] .λa,b:A.Prop.
+\ 5img class="anchor" src="icons/tick.png" id="hint_declaration_Type1"\ 6definition hint_declaration_Type1 ≝ λA:Type[1].λa,b:A.Prop.
+\ 5img class="anchor" src="icons/tick.png" id="hint_declaration_Type2"\ 6definition hint_declaration_Type2 ≝ λa,b:Type[2].Prop.
+\ 5img class="anchor" src="icons/tick.png" id="hint_declaration_CProp0"\ 6definition hint_declaration_CProp0 ≝ λA:CProp[0].λa,b:A.Prop.
+\ 5img class="anchor" src="icons/tick.png" id="hint_declaration_CProp1"\ 6definition hint_declaration_CProp1 ≝ λA:CProp[1].λa,b:A.Prop.
+\ 5img class="anchor" src="icons/tick.png" id="hint_declaration_CProp2"\ 6definition hint_declaration_CProp2 ≝ λa,b:CProp[2].Prop.
interpretation "hint_decl_Type2" 'hint_decl a b = (hint_declaration_Type2 a b).
interpretation "hint_decl_CProp2" 'hint_decl a b = (hint_declaration_CProp2 a b).