| red_view_Case ci p c brs π with RedFlags.iota flags := {
      | true with inspect (reduce c (Case_discr ci p brs :: π) _) := {
        | @exist (@exist (t,π') prf) eq with inspect (decompose_stack π') := {
          | @exist (args, ρ) prf' with cc_viewc t := {
            | ccview_construct ind' c' inst' with inspect (nth_error brs c') := {
              | exist (Some br) eqbr := rec reduce (iota_red ci.(ci_npar) p args br) π ;
              | exist None bot := False_rect _ _ } ;
            | ccview_cofix mfix idx with inspect (unfold_cofix mfix idx) := {
              | @exist (Some (narg, fn)) eq' :=
                rec reduce (tCase ci p (mkApps fn args) brs) π ;
              | @exist None bot := False_rect _ _
              } ;
            | ccview_other t ht := give (tCase ci p (mkApps t args) brs) π
            }
          }
        } ;
      | false := give (tCase ci p c brs) π
      } ;

    | red_view_Case ci p c brs π with RedFlags.iota flags := {
      | true :=
        red_view_Case_helper (inspect (reduce c (Case_discr ci p brs :: π) _))
        where
        red_view_Case_helper : { v | v = reduce c (Case_discr ci p brs :: π) _ }
                               -> { t' : term * stack | forall Σ (wfΣ : abstract_env_ext_rel X Σ), Req Σ Γ t' (_,π) /\ Pr t' π /\ Pr' t' } := {
          | @exist (@exist (t,π') prf) eq with inspect (decompose_stack π') := {
            | @exist (args, ρ) prf' with cc_viewc t := {
              | ccview_construct ind' c' inst' with inspect (nth_error brs c') := {
                | exist (Some br) eqbr := rec reduce (iota_red ci.(ci_npar) p args br) π ;
                | exist None bot := False_rect _ _ } ;
              | ccview_cofix mfix idx with inspect (unfold_cofix mfix idx) := {
                | @exist (Some (narg, fn)) eq' :=
                  rec reduce (tCase ci p (mkApps fn args) brs) π ;
                | @exist None bot := False_rect _ _
                } ;
              | ccview_other t ht := give (tCase ci p (mkApps t args) brs) π
              }
            }
          } ;
      | false := give (tCase ci p c brs) π
      } ;