interpretation "logical not" 'not x = (Not x).
-ntheorem absurd : ∀A,C:Prop.A → ¬A → C.
+nlemma absurd : ∀A,C:Prop.A → ¬A → C.
#A; #C; #H;
nnormalize;
#H1;
nelim (H1 H).
nqed.
-ntheorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
+nlemma not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
#A; #B; #H;
nnormalize;
#H1; #H2;
interpretation "logical and" 'and x y = (And x y).
-ntheorem proj1: ∀A,B:Prop.A ∧ B → A.
+nlemma proj1: ∀A,B:Prop.A ∧ B → A.
#A; #B; #H;
napply (And_ind A B ?? H);
#H1; #H2;
napply H1.
nqed.
-ntheorem proj2: ∀A,B:Prop.A ∧ B → B.
+nlemma proj2: ∀A,B:Prop.A ∧ B → B.
#A; #B; #H;
napply (And_ind A B ?? H);
#H1; #H2;
interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
-ntheorem symmetric_eq: ∀A:Type. symmetric A (eq A).
+nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
#A;
nnormalize;
#x; #y; #H;
napply (refl_eq ??).
nqed.
-ntheorem eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
+nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
#A; #x; #P; #H; #y; #H1;
napply (eq_ind ? x ? H y ?);
nrewrite < H1;
napply (refl_eq ??).
nqed.
+
+ndefinition relationT : Type → Type → Type ≝
+λA,T:Type.A → A → T.
+
+ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
+λA,T.λR.∀x,y:A.R x y = R y x.