coq intro

• Set , Prop , Lemma , Theorem , Fact , Proof , Qed , Admitted , code extraction
• Inductive , Variant , Fixpoint
• ∀ , intros , apply , apply with
• unfold , destruct , split , left , right , Show , induction
• ∃ , Negation , Equality , reasoning by Inversion , additional tactics , basic automation , functions and conversion