+
+ connect_button main#butForall_intro
+ (fun () -> source_buffer#insert "apply rule (∀_i {…} (…));\n");
+ connect_button main#butForall_elim
+ (fun () -> source_buffer#insert "apply rule (∀_e {…} (…));\n");
+ connect_button main#butExists_intro
+ (fun () -> source_buffer#insert "apply rule (∃_i {…} (…));\n");
+ connect_button main#butExists_elim
+ (fun () -> source_buffer#insert
+ "apply rule (∃_e (…) {…} […] (…));\n\t[\n\t|\n\t]\n");