convoy.v

Definition red_split_a {red: red_type} {e: aexp} (ret: red_cexp red a e): red_aexp red e :=
  match ret in red_cexp _ t e return
        (match t return exp_type t -> Type with
           | a => fun e' => red_aexp red e'
           | b => fun _  => unit
         end e)
  with
    | RCNum       n     => RANum   n
    | RCPlus  _ _ a1 a2 => RAPlus  a1 a2
    | RCMinus _ _ a1 a2 => RAMinus a1 a2
    | RCMult  _ _ a1 a2 => RAMult  a1 a2
    | RCTrue            => tt
    | RCFalse           => tt
    | RCEq    _ _ a1 a2 => tt
    | RCLe    _ _ a1 a2 => tt
    | RCNot   _   b1    => tt
    | RCAnd   _ _ b1 b2 => tt
  end.