theory Lemma
imports Main
begin
lemma I: "A --> A"
proof
assume A
show A by fact
qed
lemma shows I1: "A --> A" (is "?B --> ?C" is "?D --> ?F")
"A --> A"
and "A --> A" by auto
end