(lt (weight_map f (lift (S d) (0) u)) (g d)) ->
(le (weight_map f z) (weight_map g t)).
Intros until 1; XElim H.
-(* case 1: subst0_bref *)
+(* case 1: subst0_lref *)
Intros; XAuto.
(* case 2: subst0_fst *)
XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ltlc (**) | XAuto | XAuto | XAuto ].
(lt (weight_map f (lift (S d) (0) u)) (g d)) ->
(lt (weight_map f z) (weight_map g t)).
Intros until 1; XElim H.
-(* case 1: subst0_bref *)
+(* case 1: subst0_lref *)
Intros; XAuto.
(* case 2: subst0_fst *)
XElim k; [ XElim b | Idtac ]; Simpl; Intros;