(fun H : expr_eqb e1 e2 = true =>
 expr_ind (fun e3 : expr => forall e4 : expr, expr_eqb e3 e4 = true -> e3 = e4)
    :
  (fun (k : intconst) (e3 : expr) (H0 : expr_eqb (IntConst k) e3 = true) =>
    match e3 as e return (expr_eqb (IntConst k) e = true -> IntConst k = e) with
    (fun (ty : typename) (e3 : expr) (H0 : expr_eqb (SizeofType ty) e3 = true) =>
      match e3 as e return (expr_eqb (SizeofType ty) e = true -> SizeofType ty = e) with
        :
      | SizeofType ty0 =>
          (fun (ty1 : typename) (H1 : expr_eqb (SizeofType ty) (SizeofType ty1) = true) =>
           eq_ind_r (fun ty2 : typename => SizeofType ty2 = SizeofType ty1) eq_refl
             ((fun lemma : typename_eqb ty ty1 = true <-> ty = ty1 =>
               Morphisms.iff_impl_subrelation (typename_eqb ty ty1 = true) (ty = ty1) lemma)
                (typename_eqb_eq ty ty1) H1)) ty0
        :
      end H0)
    :
   e1 e2 H)