Matita Home

**Table of Contents**

**Table 8.1. tactics**

tactic | ::= | assume id : sterm |

| | by induction hypothesis we know term ( id ) | |

| | case id [( id : term )] … | |

| | justification done | |

| | justification let id
: term such that term
( id ) | |

| | [obtain id | conclude term] = term [auto_params | using term | using once term | proof] [done] | |

| | suppose term ( id
) [ that is equivalent to term ] | |

| | the thesis becomes term | |

| | we need to prove term
[(id
)]
[ or equivalently term] | |

| | we proceed by cases on term to prove term | |

| | we proceed by induction on term to prove term | |

| | justification we proved term
( id
) |