Goal:
    A : Type
  ============================
   (Transitive option_extends)


DEBUG:Going to execute:
intros x y z [] H

Goals:
  
  A : Type
  x : option A
  y : option A
  z : option A
  t : A
  H : option_extends (Some t) z
  ============================
   (option_extends None z)

  
  A : Type
  x : option A
  y : option A
  z : option A
  t : A
  H : option_extends (Some t) z
  ============================
   (option_extends (Some t) z)

  
  A : Type
  x : option A
  y : option A
  z : option A
  H : option_extends None z
  ============================
   (option_extends None z)


DEBUG:Going to execute:
inv H

Goals:
  
  A : Type
  x : option A
  y : option A
  z : option A
  t : A
  H : option_extends (Some t) z
  ============================
   (option_extends None z)

  
  A : Type
  x : option A
  y : option A
  z : option A
  t : A
  H : option_extends (Some t) z
  ============================
   (option_extends (Some t) z)

  
  A : Type
  x : option A
  y : option A
  z : option A
  H : option_extends None z
  ============================
   (option_extends None z)


DEBUG:Going to execute:
fun H => inversion_clear H

Goals:
  
  A : Type
  x : option A
  y : option A
  z : option A
  t : A
  H : option_extends (Some t) z
  ============================
   (option_extends None z)

  
  A : Type
  x : option A
  y : option A
  z : option A
  t : A
  H : option_extends (Some t) z
  ============================
   (option_extends (Some t) z)

  
  A : Type
  x : option A
  y : option A
  z : option A
  H : option_extends None z
  ============================
   (option_extends None z)


DEBUG:Going to execute:
inversion_clear H

Goals:
    A : Type  x : option A  y : option A  z : option A  t : A
  ============================
   (option_extends None (Some t))

    A : Type  x : option A  y : option A  z : option A  t : A
  ============================
   (option_extends (Some t) (Some t))

    A : Type  x : option A  y : option A  z : option A  t : A
  ============================
   (option_extends None (Some t))

    A : Type  x : option A  y : option A  z : option A
  ============================
   (option_extends None None)


DEBUG:Going to execute:
constructor
Level 1: evaluation returns
inversion_clear H
where
H := H
of type
ident of type tacvalue

Level 1: evaluation returns
inversion_clear H
where
H := H
of type
ident of type tacvalue

Level 1: evaluation returns
inversion_clear H
where
H := H
of type
ident of type tacvalue


Goals:
    A : Type  x : option A  y : option A  z : option A  t : A
  ============================
   (option_extends None (Some t))

    A : Type  x : option A  y : option A  z : option A  t : A
  ============================
   (option_extends (Some t) (Some t))

    A : Type  x : option A  y : option A  z : option A  t : A
  ============================
   (option_extends None (Some t))

    A : Type  x : option A  y : option A  z : option A
  ============================
   (option_extends None None)


DEBUG:Going to execute:
<coq-core.plugins.ltac::constructor@0>

COQC theories/MCSquash.v
DEBUG_CALL
COQC theories/All_Forall.v