An example of cooking

• BEFORE COOKING [The Section Path of trivial is 'S/trivial'. The only "ingredient" of trivial is A]:

      Section S.
       Variable A : Prop.
       Theorem trivial : A -> A.
        Proof.
        Exact [a:A]a.
       Qed.
      End S.
     

• AFTER COOKING (WHEN THE SECTION IS CLOSED) [The Section Path of trivial is 'trivial'. No ingredients left]:

      Coq < Print Cooked trivial.
      trivial = [A:Prop; a:A]a
           : (A:Prop)A->A