X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Ftac_weproceedbycases.html;fp=matita%2Fmatita%2Fhelp%2FC%2Ftac_weproceedbycases.html;h=0000000000000000000000000000000000000000;hb=9d5a0d55e331b348d44b6d50d3d67e62b60a0e18;hp=7b364b17cb539bcfbe89bc7d60793ea83d28c8cd;hpb=7b6ca76a0ed511b288b654729c9758277dbcd352;p=helm.git diff --git a/matita/matita/help/C/tac_weproceedbycases.html b/matita/matita/help/C/tac_weproceedbycases.html deleted file mode 100644 index 7b364b17c..000000000 --- a/matita/matita/help/C/tac_weproceedbycases.html +++ /dev/null @@ -1,6 +0,0 @@ - -we proceed by cases on
we proceed by cases on
Prev Chapter 8. Declarative Tactics Next

we proceed by cases on

we proceed by cases on t to prove P

-

Synopsis:

we proceed by cases on term to prove term

Pre-condition:

The type of t must be an inductive type and P must be identical to the current conclusion. -

Action:

It proceeds by case-analysis on t

New sequents to prove:

It opens one new sequent for each constructor of the - type of t, each with the conclusion P instantiated for the constructor.

-

Prev Up Next
we proceed by induction on Home case
\ No newline at end of file