lTheorems provable
constructively from WKL are animated by inductive inference

lMany theorems in
Reverse Mathematics are proved without or with very weak classical reasoning,
and we can transfer their proofs nearly automatically into LCM-proofs.

lAn example: Completeness theorem of the first order predicate
logic.