{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "594d1fb364424b1fa1fb08700777252b",
     "evaluated": true,
     "execution_id": "edb4c26a479b44b18b98b519dc8e7f70",
     "rolled_back": false
    }
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "\n",
       "<div class=\"coq_kernel_output_area\">\n",
       "    <pre>Proving: implication\n",
       "\n",
       "1 subgoal\n",
       "\n",
       "-------------- (1/1)\n",
       "forall A B : Prop, A -> (A -> B) -> B</pre>\n",
       "</div>\n",
       "\n",
       "<div class=\"coq_kernel_rich_cell_output coq_kernel_status_message_area\" style=\"padding: 5px 0px;\">\n",
       "    <i class=\"fa-check fa text-success\"></i>\n",
       "    <span>Cell evaluated.</span>\n",
       "</div>\n",
       "\n",
       "<div class=\"coq_kernel_rich_cell_output coq_kernel_status_message_area coq_kernel_rolled_back_status_message\" style=\"padding: 5px 0px; display: none;\">\n",
       "    <i class=\"fa-exclamation-circle fa text-info\"></i>\n",
       "    <span>Cell rolled back.</span>\n",
       "</div>\n",
       "\n",
       "<div class=\"coq_kernel_rich_cell_output coq_kernel_roll_back_controls_area\" style=\"display: none; position: relative;\">\n",
       "    <button class=\"btn btn-default btn-xs coq_kernel_roll_back_button\" onclick=\"CoqKernel.roll_back(this)\">\n",
       "        <i class=\"fa-step-backward fa\"></i>\n",
       "        <span class=\"toolbar-btn-label\">Rollback cell</span>\n",
       "    </button>\n",
       "\n",
       "    <div style=\"display: inline-block; vertical-align: middle; padding-left: 0; padding-right: 0;\">\n",
       "      <input class=\"coq_kernel_auto_roll_back_checkbox\" type=\"checkbox\" value=\"\" onchange=\"CoqKernel.toggle_auto_roll_back(this)\" checked>\n",
       "      <label\">Auto rollback</label>\n",
       "    </div>\n",
       "</div>\n"
      ],
      "text/plain": [
       "Proving: implication\n",
       "\n",
       "1 subgoal\n",
       "\n",
       "-------------- (1/1)\n",
       "forall A B : Prop, A -> (A -> B) -> B"
      ]
     },
     "execution_count": 2,
     "metadata": {
      "coq_kernel_evaluated": true,
      "coq_kernel_execution_id": "edb4c26a479b44b18b98b519dc8e7f70",
      "coq_kernel_rolled_back": false
     },
     "output_type": "execute_result"
    }
   ],
   "source": [
    "Theorem implication :\n",
    "  forall A B : Prop,\n",
    "  A ->\n",
    "  (A -> B) ->\n",
    "  B\n",
    "."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "bea3fcba3d3d42f48a527d4b7bca0cc5",
     "evaluated": true,
     "execution_id": "39ae226c45e94949bf8cf9d39709dd14",
     "rolled_back": false
    }
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "\n",
       "<div class=\"coq_kernel_output_area\">\n",
       "    <pre></pre>\n",
       "</div>\n",
       "\n",
       "<div class=\"coq_kernel_rich_cell_output coq_kernel_status_message_area\" style=\"padding: 5px 0px;\">\n",
       "    <i class=\"fa-check fa text-success\"></i>\n",
       "    <span>Cell evaluated.</span>\n",
       "</div>\n",
       "\n",
       "<div class=\"coq_kernel_rich_cell_output coq_kernel_status_message_area coq_kernel_rolled_back_status_message\" style=\"padding: 5px 0px; display: none;\">\n",
       "    <i class=\"fa-exclamation-circle fa text-info\"></i>\n",
       "    <span>Cell rolled back.</span>\n",
       "</div>\n",
       "\n",
       "<div class=\"coq_kernel_rich_cell_output coq_kernel_roll_back_controls_area\" style=\"display: none; position: relative;\">\n",
       "    <button class=\"btn btn-default btn-xs coq_kernel_roll_back_button\" onclick=\"CoqKernel.roll_back(this)\">\n",
       "        <i class=\"fa-step-backward fa\"></i>\n",
       "        <span class=\"toolbar-btn-label\">Rollback cell</span>\n",
       "    </button>\n",
       "\n",
       "    <div style=\"display: inline-block; vertical-align: middle; padding-left: 0; padding-right: 0;\">\n",
       "      <input class=\"coq_kernel_auto_roll_back_checkbox\" type=\"checkbox\" value=\"\" onchange=\"CoqKernel.toggle_auto_roll_back(this)\" checked>\n",
       "      <label\">Auto rollback</label>\n",
       "    </div>\n",
       "</div>\n"
      ],
      "text/plain": []
     },
     "execution_count": 9,
     "metadata": {
      "coq_kernel_evaluated": true,
      "coq_kernel_execution_id": "39ae226c45e94949bf8cf9d39709dd14",
      "coq_kernel_rolled_back": false
     },
     "output_type": "execute_result"
    }
   ],
   "source": [
    "Proof.\n",
    "  intros A B.\n",
    "  intros proof_of_A.\n",
    "  intros A_implies_B.\n",
    "  pose (proof_of_B := A_implies_B proof_of_A).\n",
    "  exact proof_of_B.\n",
    "Qed."
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Coq",
   "language": "coq",
   "name": "coq"
  },
  "language_info": {
   "file_extension": ".v",
   "mimetype": "text/x-coq",
   "name": "coq",
   "version": "8.6.0"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}