(* main properties with evaluations for rt-transition on terms **************)
theorem cnv_dec (h) (a) (G) (L) (T): ac_props a →
- Decidable (â\9dªG,Lâ\9d« ⊢ T ![h,a]).
+ Decidable (â\9d¨G,Lâ\9d© ⊢ T ![h,a]).
#h #a #G #L #T #Ha
@(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T #G0 #L0 #T0 #IH #G #L * * [|||| * ]
[ #s #HG #HL #HT destruct -Ha -IH