(* Main properties **********************************************************)
-theorem aaa_dec (G) (L) (T): Decidable (â\88\83A. â¦\83G,Lâ¦\84 ⊢ T ⁝ A).
+theorem aaa_dec (G) (L) (T): Decidable (â\88\83A. â\9dªG,Lâ\9d« ⊢ T ⁝ A).
#G #L #T @(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T
#G0 #L0 #T0 #IH #G #L * * [||| #p * | * ]
[ #s #HG #HL #HT destruct -IH