Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (84 entries) |

Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 entries) |

Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |

Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |

Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |

Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |

Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |

Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19 entries) |

Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |

# Global Index

## C

ComposeTo [record, in CoqWorkshop.tactics_in_terms_presentation]ComposeTo [record, in CoqWorkshop.tactics_in_terms_paper_examples]

ComposeTo11 [instance, in CoqWorkshop.tactics_in_terms_presentation]

ComposeTo11 [instance, in CoqWorkshop.tactics_in_terms_paper_examples]

ComposeTo12 [instance, in CoqWorkshop.tactics_in_terms_presentation]

ComposeTo12 [instance, in CoqWorkshop.tactics_in_terms_paper_examples]

ComposeTo21 [instance, in CoqWorkshop.tactics_in_terms_presentation]

ComposeTo21 [instance, in CoqWorkshop.tactics_in_terms_paper_examples]

ComposeTo22 [instance, in CoqWorkshop.tactics_in_terms_presentation]

ComposeTo22 [instance, in CoqWorkshop.tactics_in_terms_paper_examples]

Compose11 [axiom, in CoqWorkshop.tactics_in_terms_presentation]

Compose11 [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]

Compose12 [axiom, in CoqWorkshop.tactics_in_terms_presentation]

Compose12 [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]

Compose21 [axiom, in CoqWorkshop.tactics_in_terms_presentation]

Compose21 [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]

Compose22 [axiom, in CoqWorkshop.tactics_in_terms_presentation]

Compose22 [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]

composition [definition, in CoqWorkshop.tactics_in_terms_presentation]

composition [definition, in CoqWorkshop.tactics_in_terms_paper_examples]

## D

do_make_apply_under_binders_in_helper_helper [projection, in CoqWorkshop.tactics_in_terms_presentation]do_make_apply_under_binders_in_helper_helper [constructor, in CoqWorkshop.tactics_in_terms_presentation]

do_make_apply_under_binders_in_helper [projection, in CoqWorkshop.tactics_in_terms_presentation]

do_make_apply_under_binders_in_helper [constructor, in CoqWorkshop.tactics_in_terms_presentation]

## E

eq [inductive, in CoqWorkshop.tactics_in_terms_presentation]eq [inductive, in CoqWorkshop.tactics_in_terms_paper_examples]

eq_refl [constructor, in CoqWorkshop.tactics_in_terms_presentation]

eq_refl [constructor, in CoqWorkshop.tactics_in_terms_paper_examples]

## F

F [axiom, in CoqWorkshop.tactics_in_terms_presentation]F [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]

funext_downward_closed [definition, in CoqWorkshop.tactics_in_terms_presentation]

funext_downward_closed [definition, in CoqWorkshop.tactics_in_terms_paper_examples]

## G

G [axiom, in CoqWorkshop.tactics_in_terms_presentation]G [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]

## H

hnf_under_binders_helper [record, in CoqWorkshop.tactics_in_terms_presentation]hnf_under_binders_helper [inductive, in CoqWorkshop.tactics_in_terms_presentation]

## I

I_am_exactly_two [definition, in CoqWorkshop.tactics_in_terms_presentation]I_am_exactly_one [definition, in CoqWorkshop.tactics_in_terms_presentation]

I_am_one [definition, in CoqWorkshop.tactics_in_terms_presentation]

I_am_exactly_one [definition, in CoqWorkshop.tactics_in_terms_paper_examples]

I_am_one [definition, in CoqWorkshop.tactics_in_terms_paper_examples]

## L

Lift [definition, in CoqWorkshop.tactics_in_terms_presentation]Lift [definition, in CoqWorkshop.tactics_in_terms_paper_examples]

lift_eq [definition, in CoqWorkshop.tactics_in_terms_presentation]

lift_eq [definition, in CoqWorkshop.tactics_in_terms_paper_examples]

## M

make_apply_under_binders_in_helper_helper [record, in CoqWorkshop.tactics_in_terms_presentation]make_apply_under_binders_in_helper_helper [inductive, in CoqWorkshop.tactics_in_terms_presentation]

make_apply_under_binders_in_helper [record, in CoqWorkshop.tactics_in_terms_presentation]

make_apply_under_binders_in_helper [inductive, in CoqWorkshop.tactics_in_terms_presentation]

make_hnf_under_binders_helper [projection, in CoqWorkshop.tactics_in_terms_presentation]

make_hnf_under_binders_helper [constructor, in CoqWorkshop.tactics_in_terms_presentation]

MyF [instance, in CoqWorkshop.tactics_in_terms_presentation]

MyF [instance, in CoqWorkshop.tactics_in_terms_paper_examples]

MyG [instance, in CoqWorkshop.tactics_in_terms_presentation]

MyG [instance, in CoqWorkshop.tactics_in_terms_paper_examples]

mynotation [definition, in CoqWorkshop.tactics_in_terms_presentation]

MyNotation [record, in CoqWorkshop.tactics_in_terms_presentation]

mynotation [definition, in CoqWorkshop.tactics_in_terms_paper_examples]

MyNotation [record, in CoqWorkshop.tactics_in_terms_paper_examples]

## N

NaiveFunext [definition, in CoqWorkshop.tactics_in_terms_presentation]NaiveFunext [definition, in CoqWorkshop.tactics_in_terms_paper_examples]

## T

tactics_in_terms_paper_examples [library]tactics_in_terms_presentation [library]

t₁ [axiom, in CoqWorkshop.tactics_in_terms_presentation]

T₁ [axiom, in CoqWorkshop.tactics_in_terms_presentation]

t₁ [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]

T₁ [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]

t₂ [axiom, in CoqWorkshop.tactics_in_terms_presentation]

T₂ [axiom, in CoqWorkshop.tactics_in_terms_presentation]

t₂ [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]

T₂ [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]

T₃ [axiom, in CoqWorkshop.tactics_in_terms_presentation]

T₃ [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]

## U

unfold_me_too [definition, in CoqWorkshop.tactics_in_terms_presentation]unfold_me [definition, in CoqWorkshop.tactics_in_terms_presentation]

## other

_ = _ (type_scope) [notation, in CoqWorkshop.tactics_in_terms_presentation]_ = _ :> _ (type_scope) [notation, in CoqWorkshop.tactics_in_terms_presentation]

_ = _ (type_scope) [notation, in CoqWorkshop.tactics_in_terms_paper_examples]

_ = _ :> _ (type_scope) [notation, in CoqWorkshop.tactics_in_terms_paper_examples]

_ ∘ _ [notation, in CoqWorkshop.tactics_in_terms_presentation]

_ ∘ _ [notation, in CoqWorkshop.tactics_in_terms_paper_examples]

%% _ [notation, in CoqWorkshop.tactics_in_terms_presentation]

% _ [notation, in CoqWorkshop.tactics_in_terms_presentation]

% _ [notation, in CoqWorkshop.tactics_in_terms_paper_examples]

# Notation Index

## other

_ = _ (type_scope) [in CoqWorkshop.tactics_in_terms_presentation]_ = _ :> _ (type_scope) [in CoqWorkshop.tactics_in_terms_presentation]

_ = _ (type_scope) [in CoqWorkshop.tactics_in_terms_paper_examples]

_ = _ :> _ (type_scope) [in CoqWorkshop.tactics_in_terms_paper_examples]

_ ∘ _ [in CoqWorkshop.tactics_in_terms_presentation]

_ ∘ _ [in CoqWorkshop.tactics_in_terms_paper_examples]

%% _ [in CoqWorkshop.tactics_in_terms_presentation]

% _ [in CoqWorkshop.tactics_in_terms_presentation]

% _ [in CoqWorkshop.tactics_in_terms_paper_examples]

# Library Index

## T

tactics_in_terms_paper_examplestactics_in_terms_presentation

# Constructor Index

## D

do_make_apply_under_binders_in_helper_helper [in CoqWorkshop.tactics_in_terms_presentation]do_make_apply_under_binders_in_helper [in CoqWorkshop.tactics_in_terms_presentation]

## E

eq_refl [in CoqWorkshop.tactics_in_terms_presentation]eq_refl [in CoqWorkshop.tactics_in_terms_paper_examples]

## M

make_hnf_under_binders_helper [in CoqWorkshop.tactics_in_terms_presentation]# Axiom Index

## C

Compose11 [in CoqWorkshop.tactics_in_terms_presentation]Compose11 [in CoqWorkshop.tactics_in_terms_paper_examples]

Compose12 [in CoqWorkshop.tactics_in_terms_presentation]

Compose12 [in CoqWorkshop.tactics_in_terms_paper_examples]

Compose21 [in CoqWorkshop.tactics_in_terms_presentation]

Compose21 [in CoqWorkshop.tactics_in_terms_paper_examples]

Compose22 [in CoqWorkshop.tactics_in_terms_presentation]

Compose22 [in CoqWorkshop.tactics_in_terms_paper_examples]

## F

F [in CoqWorkshop.tactics_in_terms_presentation]F [in CoqWorkshop.tactics_in_terms_paper_examples]

## G

G [in CoqWorkshop.tactics_in_terms_presentation]G [in CoqWorkshop.tactics_in_terms_paper_examples]

## T

t₁ [in CoqWorkshop.tactics_in_terms_presentation]T₁ [in CoqWorkshop.tactics_in_terms_presentation]

t₁ [in CoqWorkshop.tactics_in_terms_paper_examples]

T₁ [in CoqWorkshop.tactics_in_terms_paper_examples]

t₂ [in CoqWorkshop.tactics_in_terms_presentation]

T₂ [in CoqWorkshop.tactics_in_terms_presentation]

t₂ [in CoqWorkshop.tactics_in_terms_paper_examples]

T₂ [in CoqWorkshop.tactics_in_terms_paper_examples]

T₃ [in CoqWorkshop.tactics_in_terms_presentation]

T₃ [in CoqWorkshop.tactics_in_terms_paper_examples]

# Inductive Index

## E

eq [in CoqWorkshop.tactics_in_terms_presentation]eq [in CoqWorkshop.tactics_in_terms_paper_examples]

## H

hnf_under_binders_helper [in CoqWorkshop.tactics_in_terms_presentation]## M

make_apply_under_binders_in_helper_helper [in CoqWorkshop.tactics_in_terms_presentation]make_apply_under_binders_in_helper [in CoqWorkshop.tactics_in_terms_presentation]

# Projection Index

## D

do_make_apply_under_binders_in_helper_helper [in CoqWorkshop.tactics_in_terms_presentation]do_make_apply_under_binders_in_helper [in CoqWorkshop.tactics_in_terms_presentation]

## M

make_hnf_under_binders_helper [in CoqWorkshop.tactics_in_terms_presentation]# Instance Index

## C

ComposeTo11 [in CoqWorkshop.tactics_in_terms_presentation]ComposeTo11 [in CoqWorkshop.tactics_in_terms_paper_examples]

ComposeTo12 [in CoqWorkshop.tactics_in_terms_presentation]

ComposeTo12 [in CoqWorkshop.tactics_in_terms_paper_examples]

ComposeTo21 [in CoqWorkshop.tactics_in_terms_presentation]

ComposeTo21 [in CoqWorkshop.tactics_in_terms_paper_examples]

ComposeTo22 [in CoqWorkshop.tactics_in_terms_presentation]

ComposeTo22 [in CoqWorkshop.tactics_in_terms_paper_examples]

## M

MyF [in CoqWorkshop.tactics_in_terms_presentation]MyF [in CoqWorkshop.tactics_in_terms_paper_examples]

MyG [in CoqWorkshop.tactics_in_terms_presentation]

MyG [in CoqWorkshop.tactics_in_terms_paper_examples]

# Definition Index

## C

composition [in CoqWorkshop.tactics_in_terms_presentation]composition [in CoqWorkshop.tactics_in_terms_paper_examples]

## F

funext_downward_closed [in CoqWorkshop.tactics_in_terms_presentation]funext_downward_closed [in CoqWorkshop.tactics_in_terms_paper_examples]

## I

I_am_exactly_two [in CoqWorkshop.tactics_in_terms_presentation]I_am_exactly_one [in CoqWorkshop.tactics_in_terms_presentation]

I_am_one [in CoqWorkshop.tactics_in_terms_presentation]

I_am_exactly_one [in CoqWorkshop.tactics_in_terms_paper_examples]

I_am_one [in CoqWorkshop.tactics_in_terms_paper_examples]

## L

Lift [in CoqWorkshop.tactics_in_terms_presentation]Lift [in CoqWorkshop.tactics_in_terms_paper_examples]

lift_eq [in CoqWorkshop.tactics_in_terms_presentation]

lift_eq [in CoqWorkshop.tactics_in_terms_paper_examples]

## M

mynotation [in CoqWorkshop.tactics_in_terms_presentation]mynotation [in CoqWorkshop.tactics_in_terms_paper_examples]

## N

NaiveFunext [in CoqWorkshop.tactics_in_terms_presentation]NaiveFunext [in CoqWorkshop.tactics_in_terms_paper_examples]

## U

unfold_me_too [in CoqWorkshop.tactics_in_terms_presentation]unfold_me [in CoqWorkshop.tactics_in_terms_presentation]

# Record Index

## C

ComposeTo [in CoqWorkshop.tactics_in_terms_presentation]ComposeTo [in CoqWorkshop.tactics_in_terms_paper_examples]

## H

hnf_under_binders_helper [in CoqWorkshop.tactics_in_terms_presentation]## M

make_apply_under_binders_in_helper_helper [in CoqWorkshop.tactics_in_terms_presentation]make_apply_under_binders_in_helper [in CoqWorkshop.tactics_in_terms_presentation]

MyNotation [in CoqWorkshop.tactics_in_terms_presentation]

MyNotation [in CoqWorkshop.tactics_in_terms_paper_examples]

Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (84 entries) |

Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 entries) |

Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |

Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |

Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |

Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |

Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |

Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19 entries) |

Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |

This page has been generated by coqdoc