Hello!
Consider the following small (typed) language with conditionals :
Inductive const :=
 BOOL (b : bool)
 INT (n : nat).
Inductive exp :=
 CONST (c : const)
 IFV (e1 e2 e3 : exp)
 ADD (e1 e2 : exp).
Inductive ty :=
 TINT
 TBOOL.
The typing judgement is given by:
Inductive hastype : exp > ty > Prop :=
 T_BOOL : forall b, hastype (CONST b) TBOOL
 T_INT : forall n, hastype (CONST (INT n)) TINT
 T_IFV : forall e1 e2 e3 ty,
hastype e1 TBOOL >
hastype e2 ty >
hastype e3 ty >
hastype (IFV e1 e2 e3) ty
 T_ADD : forall e1 e2,
hastype e1 TINT >
hastype e2 TINT >
hastype (ADD e1 e2) TINT.
Now define a program transformation which consists in lifting the IFV
nodes outside of nested expressions to the top level of the term. We define a type for the target of the transformation:
Inductive uexp :=
 UCONST (c : const)
 UADD (e1 e2 : uexp).
Inductive sexp :=
 SIFV (e1 : bool) (e2 e3 : sexp)
 SEXP (e : uexp).
(Note that in this type the condition of SIFV
is always a literal boolean.)
The transformation itself is defined by:
Fixpoint bool_of_exp e :=
match e with
 UCONST (BOOL b) => Some b
 _ => None
end.
Definition dummy := SEXP (UCONST (INT 42)).
Fixpoint push (e : exp) (f : uexp > sexp) : sexp :=
match e with
 CONST c => f (UCONST c)
 IFV e1 e2 e3 =>
push e1 (fun e1 => match bool_of_exp e1 with
 Some b => SIFV b (push e2 f) (push e3 f)
 None => dummy (* cannot happen if [e] is well typed *)
end)
 ADD e1 e2 =>
push e1 (fun e1 => push e2 (fun e2 => f (UADD e1 e2)))
end.
Definition doit e := push e SEXP.
For example, doit
rewrites (if true then 1 else 2) + 5
to if true then 1 + 5 else 2 + 5
(in obvious notation).
QUESTION: When reasoning about this function, I would like to deduce that the dummy
branch is never taken if the input of the push
is welltyped, but I do not see how to do it (or even how to write it in Coq). I can imagine two possible approaches:

try to give a stronger signature to
push
so that it becomes â€śtypepreservingâ€ť, but this would involve passing proofs of welltypedness around and I donâ€™t know how to do that. 
make
push
return anoption
, withNone
used for the â€śbadlytypedâ€ť case, but then I am afraid of all the extra bookkeeping that will imply in every statement (and proof) involving it.
Does this look reasonable? Should I be looking along these lines or should I try a completely different approach?
Any suggestions or comments would be appreciated!
Cheers,
Nicolas