X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Fhtml%2Ftac_existselim.html;fp=matita%2Fmatita%2Fhelp%2FC%2Fhtml%2Ftac_existselim.html;h=939f714fe82bf0c5c869b51269c7e14d3fd78ae9;hb=9d5a0d55e331b348d44b6d50d3d67e62b60a0e18;hp=0000000000000000000000000000000000000000;hpb=7b6ca76a0ed511b288b654729c9758277dbcd352;p=helm.git diff --git a/matita/matita/help/C/html/tac_existselim.html b/matita/matita/help/C/html/tac_existselim.html new file mode 100644 index 000000000..939f714fe --- /dev/null +++ b/matita/matita/help/C/html/tac_existselim.html @@ -0,0 +1,11 @@ + +let such that
let such that
Prev Chapter 8. Declarative Tactics Next

let such that

justification let x:T such that P (H) +

+

Synopsis:

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

Pre-condition:

+ None. +

Action:

+ It applies the left introduction rule of the existential quantifier on the formula ∃ x. P(x) (in Natural Deduction this corresponds to the elimination rule for the quantifier). +

New sequent to prove:

A new sequent with ∃ x. P(x) as the conclusion is opened and then immediately closed using the given justification. A new sequent with the conclusion of the sequent on which this tactic was applied is opened, and two new hypotheses x : T and H : P are added to the context.

+

Prev Up Next
we proved Home we have
\ No newline at end of file