-
∣∣, 9.2
- ;, 9.2
- ;[…∣…∣…], 9.2
- abstract, 9.2
- absurd, 8.4.1
- admit, 8.3.17
- apply, 8.3.6
- apply … with, 8.3.6
- apply … in, 8.3.9
- assert, 8.3.8
- assert as, 8.3.8
- assert by, 8.3.8
- assumption, 8.3.1
- auto, 8.12.1
- autorewrite, 8.12.13
- autounfold, 8.12.3
- case, 8.7.2
- case_eq, 8.7.2
- cbv, 8.5.1
- change, 8.3.12
- change … in, 8.3.12
- classical_left, 8.11.1
- classical_right, 8.11.1
- clear, 8.3.2
- clear dependent, 8.3.2
- clearbody, 8.3.2
- cofix, 8.3.14
- compare, 8.9.2
- compute, 8.5.1, 8.5.1
- congruence, 8.12.8
- constr_eq, 8.3.18
- constructor, 8.6.1
- contradict, 8.4.3
- contradiction, 8.4.2
- cut, 8.3.8
- cutrewrite, 8.8.2
- decide equality, 8.9.1
- decompose, 8.7.6
- decompose record, 8.7.6
- decompose sum, 8.7.6
- dependent destruction, 8.7.5
- dependent induction, 8.7.5
- dependent induction … generalizing, 8.7.5
- dependent inversion, 8.10.1
- dependent inversion … as , 8.10.1
- dependent inversion … as … with, 8.10.1
- dependent inversion … with, 8.10.1
- dependent inversion_clear, 8.10.1
- dependent inversion_clear … as, 8.10.1
- dependent inversion_clear … as … with, 8.10.1
- dependent inversion_clear … with, 8.10.1
- dependent rewrite ->, 8.9.6
- dependent rewrite <-, 8.9.6
- destruct, 8.7.2
- discriminate, 8.9.3
- discrR, 3.2.4
- do, 9.2
- eapply, 8.3.6, 10.2
- eapply … in, 8.3.9
- eassumption, 8.3.1
- eauto, 8.12.2
- ecase, 8.7.2
- econstructor, 8.6.1
- edestruct, 8.7.2
- ediscriminate, 8.9.3
- eelim, 8.7.1
- eexact, 8.2.1
- eexists, 8.6.1
- einduction, 8.7.1
- einjection, 8.9.4
- eleft, 8.6.1
- elim … using, 8.7.1
- elimtype, 8.7.1
- erewrite, 8.8.1
- eright, 8.6.1
- esimplify_eq, 8.9.5
- esplit, 8.6.1
- evar, 8.3.15
- exact, 8.2.1
- exfalso, 8.4.4
- exists, 8.6.1
- f_equal, 8.8.9
- fail, 9.2
- field, 8.12.11, 23.7
- field_simplify, 8.12.11, 23.7
- field_simplify_eq, 8.12.11, 23.7
- first, 9.2
- firstorder, 8.12.7
- firstorder tactic, 8.12.7
- firstorder using, 8.12.7
- firstorder with, 8.12.7
- fix, 8.3.13
- fold, 8.5.6
- fourier, 8.12.12
- functional induction, 8.7.7, 10.4
- generalize, 8.3.10
- generalize dependent, 8.3.10
| - has_evar, 8.3.20
- hnf, 8.5.3
- idtac, 9.2
- induction, 8.7.1
- info, 9.2
- injection, 8.9.4
- injection … as, 8.9.4
- instantiate, 8.3.16
- intro, 8.3.5
- intro after, 8.3.5
- intro at bottom, 8.3.5
- intro at top, 8.3.5
- intro before, 8.3.5
- intros, 8.3.5
- intros intro_pattern, 8.7.3
- intros until, 8.3.5, 8.3.5
- intuition, 8.12.5
- inversion, 8.10.1, 10.5
- inversion … as, 8.10.1
- inversion … as … in, 8.10.1
- inversion … in, 8.10.1
- inversion … using, 8.10.1
- inversion … using … in, 8.10.1
- inversion_clear, 8.10.1
- inversion_clear … as … in, 8.10.1
- inversion_clear … in, 8.10.1
- inversion_cleardots as, 8.10.1
- is_evar, 8.3.19
- is_var, 8.3.21
- lapply, 8.3.6
- lazy, 8.5.1
- left, 8.6.1
- legacy field, 23.9.3
- legacy ring, 23.9.1
- lia, 20.3
- move, 8.3.3
- nsatz, 24.1
- omega, 8.12.9, 19.1
- pattern, 8.5.7
- pose, 8.3.7
- pose proof, 8.3.8, 8.3.8
- progress, 9.2
- psatz, 20.1
- quote, 8.10.4, 10.8
- red, 8.5.2
- refine, 8.2.2, 10.1
- reflexivity, 8.8.4
- remember, 8.3.7
- rename, 8.3.4
- repeat, 9.2
- replace … with, 8.8.3
- revert, 8.3.11
- revert dependent, 8.3.11
- rewrite, 8.8.1
- rewrite ->, 8.8.1
- rewrite <-, 8.8.1
- rewrite … at, 8.8.1
- rewrite … by, 8.8.1
- rewrite … in, 8.8.1
- right, 8.6.1
- ring, 8.12.10, 23, 23.4
- ring_simplify, 8.12.10, 23.4
- rtauto, 8.12.6
- set, 8.3.7
- setoid_replace, 25
- simpl, 8.5.4
- simpl … in, 8.5.4
- simple apply, 8.3.6
- simple apply … in, 8.3.9
- simple destruct, 8.7.2
- simple eapply … in, 8.3.9
- simple induction, 8.7.1
- simple inversion, 8.10.1
- simple inversion … as, 8.10.1
- simplify_eq, 8.9.5
- solve, 9.2
- specialize, 8.3.8
- split, 8.6.1
- split_Rabs, 3.2.4
- split_Rmult, 3.2.4
- stepl, 8.8.8
- stepr, 8.8.8
- subst, 8.8.7
- symmetry, 8.8.5
- symmetry in, 8.8.5
- tauto, 8.12.4
- transitivity, 8.8.6
- trivial, 8.12.1
- try, 9.2
- unfold, 8.5.5
- unfold … in, 8.5.5
- vm_compute, 8.5.1, 8.5.1
|
