From 5dedda34c5f7b80d10bff717c5e6f90d0b92a5c7 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 3 Jun 2009 14:42:12 +0000 Subject: [PATCH] not_to_not --- helm/software/matita/library/logic/connectives.ma | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/helm/software/matita/library/logic/connectives.ma b/helm/software/matita/library/logic/connectives.ma index fcd046277..76d032316 100644 --- a/helm/software/matita/library/logic/connectives.ma +++ b/helm/software/matita/library/logic/connectives.ma @@ -32,6 +32,12 @@ qed. default "absurd" cic:/matita/logic/connectives/absurd.con. +theorem not_to_not : \forall A,B:Prop. (A → B) \to ¬B →¬A. +intros.unfold.intro.apply H1.apply (H H2). +qed. + +default "absurd" cic:/matita/logic/connectives/absurd.con. + inductive And (A,B:Prop) : Prop \def conj : A \to B \to (And A B). -- 2.39.2