nlemma proj1: ∀A,B:Prop.A ∧ B → A.
#A; #B; #H;
+ (* \ldots al posto di ??? *)
napply (And_ind A B … H);
#H1; #H2;
napply H1.
ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
ndefinition iff ≝
-λA,B.(A -> B) ∧ (B -> A).
+λA,B.(A → B) ∧ (B → A).
(* higher_order_defs/relations *)
ninductive list (A:Type) : Type ≝
nil: list A
-| cons: A -> list A -> list A.
+| cons: A → list A → list A.
nlet rec append A (l1: list A) l2 on l1 ≝
match l1 with
- [ nil => l2
- | (cons hd tl) => cons A hd (append A tl l2) ].
+ [ nil ⇒ l2
+ | (cons hd tl) ⇒ cons A hd (append A tl l2) ].
notation "hvbox(hd break :: tl)"
right associative with precedence 47