diff --git a/frontend/src/domain/visual-proof-editor/components/visual-proof-editor-parameter-identifier-selector.tsx b/frontend/src/domain/visual-proof-editor/components/visual-proof-editor-parameter-identifier-selector.tsx
new file mode 100644
index 0000000..cabf40e
--- /dev/null
+++ b/frontend/src/domain/visual-proof-editor/components/visual-proof-editor-parameter-identifier-selector.tsx
@@ -0,0 +1,207 @@
+import { get_free_parameters, Identifier, instantiate_free_parameter_by_index, Prop } from 'alice';
+import { Select, Space } from 'antd';
+import React, { Fragment, ReactElement, useCallback, useEffect, useRef, useState } from 'react';
+
+interface VisualProofEditorParameterIdentifierSelectorProps {
+    prop: Prop;
+    options: { [name: string]: Identifier[] },
+    onAllSelect: (prop: Prop) => void;
+    getPopupContainer?: () => HTMLElement;
+}
+
+interface RenderPropResult {
+    node: ReactElement;
+    newIndex: number;
+}
+
+type RenderProp = (prop: Prop, index: number, boundIdentifiers: string[]) => RenderPropResult;
+
+export function VisualProofEditorParameterIdentifierSelector(props: VisualProofEditorParameterIdentifierSelectorProps) {
+    const {
+        prop,
+        options,
+        onAllSelect,
+        getPopupContainer,
+    } = props;
+
+    const containerRef = useRef<HTMLDivElement | null>(null);
+    const [paramMapping, setParamMapping] = useState<{ [idx: number]: number } | null>(null);
+
+    useEffect(() => {
+        const selectableParamSize = get_free_parameters(prop)
+            .filter((param) => param.kind === 'Uninstantiated')
+            .length;
+
+        setParamMapping(Object.assign({}, Array(selectableParamSize).fill(0)));
+    }, [prop]);
+
+    useEffect(() => {
+
+        if (!paramMapping) {
+            return;
+        }
+
+        const params = get_free_parameters(prop);
+        let instantiatedProp = { ...prop };
+        for (const [paramIndex, identifierIndex] of Object.entries(paramMapping)) {
+            const param = params[parseInt(paramIndex)];
+            const paramName = param.kind === 'Instantiated' ? param.value.name : param.value;
+
+            instantiatedProp = instantiate_free_parameter_by_index(
+                instantiatedProp,
+                parseInt(paramIndex),
+                options[paramName][identifierIndex],
+            );
+        }
+
+        onAllSelect(instantiatedProp);
+    }, [paramMapping]);
+
+    const renderProp: RenderProp = (prop: Prop, index: number, boundIdentifiers: string[]) => {
+
+        const handlePrimitive = useCallback((symbol: string, index: number) => {
+            return {
+                node: (<span>{symbol}</span>),
+                newIndex: index,
+            };
+        }, []);
+
+        const handleBinaryConnective = useCallback((symbol: string, prop: Prop & { kind: 'And' | 'Or' | 'Impl' }, index: number, boundIdentifiers: string[]) => {
+            const fst = renderProp(prop, index, [...boundIdentifiers]);
+            const snd = renderProp(prop, fst.newIndex, boundIdentifiers);
+
+            const node = (
+                <>
+                    {fst.node}
+                    <span>
+                        {symbol}
+                    </span>
+                    {snd.node}
+                </>
+            );
+
+            return {
+                node,
+                newIndex: snd.newIndex,
+            };
+        }, []);
+
+        const handleQuantifier = useCallback((symbol: string, prop: Prop & { kind: 'ForAll' | 'Exists' }, index: number, boundIdentifiers: string[]) => {
+            const body = renderProp(
+                prop.value.body,
+                index,
+                [...boundIdentifiers, prop.value.object_ident],
+            );
+
+            const node = (
+                <>
+                    <span>{symbol}</span>
+                    <span>{prop.value.object_ident}</span>
+                    <span>:</span>
+                    <span>{prop.value.object_type_ident}</span>
+                    <span>. </span>
+                    <span>{body.node}</span>
+                </>
+            );
+
+            return {
+                node,
+                newIndex: body.newIndex,
+            };
+        }, []);
+
+        const handleAtom = useCallback((prop: Prop & { kind: 'Atom' }, index: number, boundIdentifiers: string[]) => {
+            const params = prop.value[1];
+
+            const paramNodes = [];
+            for (const param of params) {
+                const paramIndex = index;
+                const paramName = param.kind === 'Instantiated' ? param.value.name : param.value;
+
+                if (param.kind === 'Instantiated' || boundIdentifiers.includes(paramName)) {
+                    paramNodes.push(<span>{paramName}</span>);
+
+                    index++;
+                    continue;
+                }
+
+                const identOptions = options[paramName];
+
+                if (!identOptions || identOptions.length === 0) {
+                    throw new Error(`No options for name ${paramName}.`);
+                }
+
+                const selectionOptions = identOptions
+                    .map((option, i) => ({
+                        label: `${option.name} - ${option.unique_id}`,
+                        value: i,
+                    }));
+
+                const handleSelect = (idx: number) => {
+                    setParamMapping({
+                        ...paramMapping,
+                        [paramIndex]: idx,
+                    });
+                };
+
+                const node = (
+                    <Space wrap>
+                        <Select
+                            getPopupContainer={getPopupContainer}
+                            onChange={handleSelect}
+                            defaultValue={0}
+                            options={selectionOptions}
+                        />
+                    </Space>
+                );
+
+                paramNodes.push(node);
+                index++;
+            }
+
+            const propName = prop.value[0];
+
+            const node = (
+                <>
+                    <span>{propName}</span>
+                    {paramNodes.length > 0 && (
+                        <>
+                            <span>(</span>
+                            {
+                                paramNodes.map((node, i) => (
+                                    <Fragment key={i}>
+                                        {i > 0 && <span>, </span>}
+                                        {node}
+                                    </Fragment>
+                                ))
+                            }
+                            <span>)</span>
+                        </>
+                    )}
+                </>
+            );
+
+            return {
+                node,
+                newIndex: index,
+            }
+        }, []);
+
+        switch (prop.kind) {
+            case 'True': return handlePrimitive('⊤', index);
+            case 'False': return handlePrimitive('⊥', index);
+            case 'And': return handleBinaryConnective('∧', prop, index, boundIdentifiers);
+            case 'Or': return handleBinaryConnective('∨', prop, index, boundIdentifiers);
+            case 'Impl': return handleBinaryConnective('⊃', prop, index, boundIdentifiers);
+            case 'ForAll': return handleQuantifier('∀', prop, index, boundIdentifiers);
+            case 'Exists': return handleQuantifier('∃', prop, index, boundIdentifiers);
+            case 'Atom': return handleAtom(prop, index, boundIdentifiers);
+        }
+    };
+
+    return (
+        <div ref={containerRef}>
+            {renderProp(prop, 0, []).node}
+        </div>
+    );
+}
\ No newline at end of file
diff --git a/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/and-elim-fst-rule-handler.ts b/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/and-elim-fst-rule-handler.ts
index 42db537..43357f6 100644
--- a/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/and-elim-fst-rule-handler.ts
+++ b/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/and-elim-fst-rule-handler.ts
@@ -1,6 +1,5 @@
 import { v4 } from 'uuid';
 import { ProofRuleHandlerResult, VisualProofEditorRuleHandlerParams } from '..';
-import Swal from 'sweetalert2';
 import { ProofRuleHandler } from './proof-rule-handler';
 import { Prop } from 'alice';
 import { createEmptyVisualProofEditorProofTreeFromProp } from '../../lib/visual-proof-editor-proof-tree';
@@ -18,7 +17,7 @@ export class AndElimFstRuleHandler extends ProofRuleHandler {
     }
 
     protected async handleRuleUpwards(params: VisualProofEditorRuleHandlerParams): Promise<ProofRuleHandlerResult | undefined> {
-        const { selectedProofTreeNodes, error } = params;
+        const { selectedProofTreeNodes, error, assumptions } = params;
 
         if (selectedProofTreeNodes.length !== 1) {
             error('Cannot apply this rule on multiple nodes.');
@@ -33,20 +32,17 @@ export class AndElimFstRuleHandler extends ProofRuleHandler {
             return;
         }
 
-        const secondComponentResult = await Swal.fire({
-            title: 'Enter second component of conjunction.',
-            input: 'text',
+        const secondComponent = await this.promptProp({
+            title: 'Enter second component of conjunction',
             inputPlaceholder: 'B',
-            showCloseButton: true,
+            assumptions,
+            error,
         });
 
-        let secondComponent = secondComponentResult.value;
         if (!secondComponent) {
             return;
         }
 
-        secondComponent = this.parseProp(secondComponent);
-
         const conjunction: Prop = { kind: 'And', value: [conclusion.value, secondComponent] };
 
         return {
diff --git a/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/and-elim-snd-rule-handler.ts b/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/and-elim-snd-rule-handler.ts
index 8d8dcb7..2c60a0c 100644
--- a/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/and-elim-snd-rule-handler.ts
+++ b/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/and-elim-snd-rule-handler.ts
@@ -1,6 +1,5 @@
 import { v4 } from 'uuid';
 import { ProofRuleHandlerResult, VisualProofEditorRuleHandlerParams } from '..';
-import Swal from 'sweetalert2';
 import { ProofRuleHandler } from './proof-rule-handler';
 import { Prop } from 'alice';
 import { createEmptyVisualProofEditorProofTreeFromProp } from '../../lib/visual-proof-editor-proof-tree';
@@ -18,7 +17,7 @@ export class AndElimSndRuleHandler extends ProofRuleHandler {
     }
 
     protected async handleRuleUpwards(params: VisualProofEditorRuleHandlerParams): Promise<ProofRuleHandlerResult | undefined> {
-        const { selectedProofTreeNodes, error } = params;
+        const { selectedProofTreeNodes, assumptions, error } = params;
 
         if (selectedProofTreeNodes.length !== 1) {
             error('Cannot apply this rule on multiple nodes.');
@@ -33,20 +32,17 @@ export class AndElimSndRuleHandler extends ProofRuleHandler {
             return;
         }
 
-        const firstComponentResult = await Swal.fire({
-            title: 'Enter first component of conjunction.',
-            input: 'text',
+        const firstConclusion = await this.promptProp({
+            title: 'Enter first component of conjunction',
             inputPlaceholder: 'A',
-            showCloseButton: true,
+            assumptions,
+            error,
         });
 
-        let firstConclusion = firstComponentResult.value;
         if (!firstConclusion) {
             return;
         }
 
-        firstConclusion = this.parseProp(firstConclusion);
-
         const conjunction: Prop = { kind: 'And', value: [firstConclusion, conclusion.value] };
 
         return {
diff --git a/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/exists-elim-rule-handler.ts b/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/exists-elim-rule-handler.ts
index 4668a49..b013f07 100644
--- a/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/exists-elim-rule-handler.ts
+++ b/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/exists-elim-rule-handler.ts
@@ -1,4 +1,3 @@
-import Swal from 'sweetalert2';
 import { instantiate_free_parameter } from 'alice';
 import { v4 } from 'uuid';
 import { VisualProofEditorRuleHandlerParams, ProofRuleHandlerResult } from '..';
@@ -26,6 +25,7 @@ export class ExistsElimRuleHandler extends ProofRuleHandler {
             selectedProofTreeNodes,
             generateIdentifier,
             generateUniqueNumber,
+            assumptions,
             error,
         } = params;
 
@@ -42,19 +42,17 @@ export class ExistsElimRuleHandler extends ProofRuleHandler {
             return;
         }
 
-        let existsProp = (await Swal.fire({
+        const existsProp = await this.promptProp({
             title: 'Enter existential quantification you want to eliminate.',
-            input: 'text',
             inputPlaceholder: '∃x:t. A(x)',
-            showCloseButton: true,
-        })).value;
+            assumptions,
+            error,
+        });
 
         if (!existsProp) {
             return;
         }
 
-        existsProp = this.parseProp(existsProp);
-
         if (existsProp.kind !== 'Exists') {
             error('You did not enter an existential quantification.');
             return;
@@ -101,6 +99,7 @@ export class ExistsElimRuleHandler extends ProofRuleHandler {
             selectedProofTreeNodes,
             generateIdentifier,
             generateUniqueNumber,
+            assumptions,
             error,
         } = params;
 
@@ -124,23 +123,19 @@ export class ExistsElimRuleHandler extends ProofRuleHandler {
             return;
         }
 
-        // ask for new conclusion
-        let newConclusion = (await Swal.fire({
+        const newConclusion = await this.promptProp({
             title: 'Enter new conclusion',
-            input: 'text',
             inputPlaceholder: 'C',
-            showCloseButton: true,
-        })).value;
+            assumptions,
+            error,
+        });
 
         if (!newConclusion) {
-            return this.createEmptyProofRuleHandlerResult();
+            return;
         }
 
-        newConclusion = this.parseProp(newConclusion);
-
-
         // TODO check that free parameter does not escape scope
-
+        // Let that handle the type checker
 
         const { object_ident, object_type_ident, body } = propConclusion.value;
 
diff --git a/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/false-elim-rule-handler.ts b/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/false-elim-rule-handler.ts
index 362dd47..74dea0d 100644
--- a/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/false-elim-rule-handler.ts
+++ b/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/false-elim-rule-handler.ts
@@ -1,4 +1,3 @@
-import Swal from 'sweetalert2';
 import { VisualProofEditorRuleHandlerParams, ProofRuleHandlerResult } from '..';
 import { ProofRuleHandler } from './proof-rule-handler';
 import { v4 } from 'uuid';
@@ -43,7 +42,7 @@ export class FalseElimRuleHandler extends ProofRuleHandler {
     }
 
     protected async handleRuleDownards(params: VisualProofEditorRuleHandlerParams): Promise<ProofRuleHandlerResult | undefined> {
-        const { selectedProofTreeNodes, error } = params;
+        const { selectedProofTreeNodes, assumptions, error } = params;
 
         if (selectedProofTreeNodes.length !== 1) {
             error('Cannot apply this rule on multiple nodes.');
@@ -65,21 +64,17 @@ export class FalseElimRuleHandler extends ProofRuleHandler {
             return;
         }
 
-        const newConclusionResult = await Swal.fire({
+        const newConclusion = await this.promptProp({
             title: 'Enter new conclusion.',
-            input: 'text',
-            inputPlaceholder: 'A',
-            showCloseButton: true,
+            inputPlaceholder: 'C',
+            assumptions,
+            error,
         });
 
-        let newConclusion = newConclusionResult.value;
-
         if (!newConclusion) {
             return;
         }
 
-        newConclusion = this.parseProp(newConclusion);
-
         return {
             additionalAssumptions: [],
             removedReasoingContextIds: [],
diff --git a/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/impl-elim-rule-handler.ts b/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/impl-elim-rule-handler.ts
index 6176724..9e8faa4 100644
--- a/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/impl-elim-rule-handler.ts
+++ b/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/impl-elim-rule-handler.ts
@@ -1,7 +1,6 @@
 import { v4 } from 'uuid';
 import { VisualProofEditorRuleHandlerParams, ProofRuleHandlerResult } from '..';
 import { ProofRuleHandler } from './proof-rule-handler';
-import Swal from 'sweetalert2';
 import { isEqual } from 'lodash';
 import { createEmptyVisualProofEditorProofTreeFromProp } from '../../lib/visual-proof-editor-proof-tree';
 
@@ -19,7 +18,7 @@ export class ImplElimRuleHandler extends ProofRuleHandler {
     }
 
     protected async handleRuleUpwards(params: VisualProofEditorRuleHandlerParams): Promise<ProofRuleHandlerResult | undefined> {
-        const { selectedProofTreeNodes, error } = params;
+        const { selectedProofTreeNodes, assumptions, error } = params;
 
         if (selectedProofTreeNodes.length !== 1) {
             error('Cannot apply rule on this node.');
@@ -34,19 +33,17 @@ export class ImplElimRuleHandler extends ProofRuleHandler {
             return;
         }
 
-        let implAntecedent = (await Swal.fire({
+        const implAntecedent = await this.promptProp({
             title: 'Enter antecedent of implication.',
-            input: 'text',
             inputPlaceholder: 'A',
-            showCloseButton: true,
-        })).value;
+            assumptions,
+            error,
+        });
 
         if (!implAntecedent) {
             return;
         }
 
-        implAntecedent = this.parseProp(implAntecedent);
-
         return {
             additionalAssumptions: [],
             removedReasoingContextIds: [],
diff --git a/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/or-elim-rule-handler.ts b/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/or-elim-rule-handler.ts
index c86ebe7..859069b 100644
--- a/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/or-elim-rule-handler.ts
+++ b/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/or-elim-rule-handler.ts
@@ -1,4 +1,3 @@
-import Swal from 'sweetalert2';
 import { Identifier, Prop } from 'alice';
 import { v4 } from 'uuid';
 import { VisualProofEditorRuleHandlerParams, ProofRuleHandlerResult, AssumptionContext } from '..';
@@ -28,6 +27,7 @@ export class OrElimRuleHandler extends ProofRuleHandler {
             selectedProofTreeNodes,
             generateIdentifier,
             generateUniqueNumber,
+            assumptions,
             error,
         } = params;
 
@@ -44,20 +44,17 @@ export class OrElimRuleHandler extends ProofRuleHandler {
             return;
         }
 
-        // ask for disjunction
-        let disjunction = (await Swal.fire({
+        const disjunction = await this.promptProp({
             title: 'Enter the disjunction you want to eliminate from.',
-            input: 'text',
             inputPlaceholder: 'A v B',
-            showCloseButton: true,
-        })).value;
+            assumptions,
+            error,
+        });
 
         if (!disjunction) {
             return;
         }
 
-        disjunction = this.parseProp(disjunction);
-
         if (disjunction.kind !== 'Or') {
             error('Your input is not a disjunction.');
             return;
@@ -99,6 +96,7 @@ export class OrElimRuleHandler extends ProofRuleHandler {
             selectedProofTreeNodes,
             generateIdentifier,
             generateUniqueNumber,
+            assumptions,
             error,
         } = params;
 
@@ -122,20 +120,17 @@ export class OrElimRuleHandler extends ProofRuleHandler {
             return;
         }
 
-        // ask for new conclusion
-        const newConclusionPromptResult = await Swal.fire({
+        const newConclusion = await this.promptProp({
             title: 'Enter new conclusion',
-            input: 'text',
             inputPlaceholder: 'C',
-            showCloseButton: true,
+            assumptions,
+            error,
         });
 
-        if (!newConclusionPromptResult.isConfirmed) {
+        if (!newConclusion) {
             return;
         }
 
-        const newConclusion = this.parseProp(newConclusionPromptResult.value);
-
         const nodeId = v4();
 
         const additionalAssumptions = createProofRuleHandlerResultAssumptionContexts({
diff --git a/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/or-intro-fst-rule-handler.ts b/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/or-intro-fst-rule-handler.ts
index e703293..1fbfa26 100644
--- a/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/or-intro-fst-rule-handler.ts
+++ b/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/or-intro-fst-rule-handler.ts
@@ -1,4 +1,3 @@
-import Swal from 'sweetalert2';
 import { VisualProofEditorRuleHandlerParams, ProofRuleHandlerResult } from '..';
 import { ProofRuleHandler } from './proof-rule-handler';
 import { v4 } from 'uuid';
@@ -59,7 +58,7 @@ export class OrIntroFstRuleHandler extends ProofRuleHandler {
     }
 
     protected async handleRuleDownards(params: VisualProofEditorRuleHandlerParams): Promise<ProofRuleHandlerResult | undefined> {
-        const { selectedProofTreeNodes, error } = params;
+        const { selectedProofTreeNodes, assumptions, error } = params;
 
         if (selectedProofTreeNodes.length !== 1) {
             error('Cannot apply this rule on multiple nodes.');
@@ -74,21 +73,18 @@ export class OrIntroFstRuleHandler extends ProofRuleHandler {
             return;
         }
 
-        const secondComponentResult = await Swal.fire({
+        // secondComponent = this.parseProp(secondComponent);
+        const secondComponent = await this.promptProp({
             title: 'Enter second component of disjunction.',
-            input: 'text',
             inputPlaceholder: 'B',
-            showCloseButton: true,
+            assumptions,
+            error,
         });
 
-        let secondComponent = secondComponentResult.value;
-
         if (!secondComponent) {
             return;
         }
 
-        secondComponent = this.parseProp(secondComponent);
-
         return {
             additionalAssumptions: [],
             newReasoningContexts: [],
diff --git a/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/or-intro-snd-rule-handler.ts b/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/or-intro-snd-rule-handler.ts
index 68da116..dc90092 100644
--- a/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/or-intro-snd-rule-handler.ts
+++ b/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/or-intro-snd-rule-handler.ts
@@ -1,4 +1,3 @@
-import Swal from 'sweetalert2';
 import { VisualProofEditorRuleHandlerParams, ProofRuleHandlerResult } from '..';
 import { ProofRuleHandler } from './proof-rule-handler';
 import { v4 } from 'uuid';
@@ -59,7 +58,7 @@ export class OrIntroSndRuleHandler extends ProofRuleHandler {
     }
 
     protected async handleRuleDownards(params: VisualProofEditorRuleHandlerParams): Promise<ProofRuleHandlerResult | undefined> {
-        const { selectedProofTreeNodes, error } = params;
+        const { selectedProofTreeNodes, assumptions, error } = params;
 
         if (selectedProofTreeNodes.length !== 1) {
             error('Cannot apply rule on this node.');
@@ -74,21 +73,17 @@ export class OrIntroSndRuleHandler extends ProofRuleHandler {
             return;
         }
 
-        const firstComponentResult = await Swal.fire({
+        const firstComponent = await this.promptProp({
             title: 'Enter first component of disjunction.',
-            input: 'text',
             inputPlaceholder: 'A',
-            showCloseButton: true,
+            assumptions,
+            error,
         });
 
-        let firstComponent = firstComponentResult.value;
-
         if (!firstComponent) {
             return;
         }
 
-        firstComponent = this.parseProp(firstComponent);
-
         return {
             additionalAssumptions: [],
             newReasoningContexts: [],
diff --git a/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/proof-rule-handler.ts b/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/proof-rule-handler.ts
index f6f3609..1f32b98 100644
--- a/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/proof-rule-handler.ts
+++ b/frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/proof-rule-handler.ts
@@ -1,5 +1,19 @@
-import { parse_prop, Prop } from 'alice';
-import { ProofRuleHandlerResult, VisualProofEditorRuleHandlerParams } from '..';
+import { get_free_parameters, Identifier, instantiate_free_parameter, parse_prop, Prop } from 'alice';
+import { AssumptionContext, ProofRuleHandlerResult, VisualProofEditorRuleHandlerParams } from '..';
+import Swal from 'sweetalert2';
+import { uniq } from 'lodash';
+import withReactContent from 'sweetalert2-react-content';
+import React from 'react';
+import { VisualProofEditorParameterIdentifierSelector } from '../../components/visual-proof-editor-parameter-identifier-selector';
+
+const ReactSwal = withReactContent(Swal);
+
+interface PromptPropOptions {
+    title: string;
+    inputPlaceholder?: string;
+    assumptions: AssumptionContext[];
+    error: (msg: string) => void;
+}
 
 export abstract class ProofRuleHandler {
 
@@ -9,6 +23,90 @@ export abstract class ProofRuleHandler {
 
     protected abstract handleRuleDownards(params: VisualProofEditorRuleHandlerParams): Promise<ProofRuleHandlerResult | undefined>;
 
+    protected async promptProp(options: PromptPropOptions): Promise<Prop | null> {
+        const {
+            title,
+            inputPlaceholder,
+            assumptions,
+            error,
+        } = options;
+
+        let prop = (await Swal.fire({
+            title,
+            inputPlaceholder,
+            input: 'text',
+            showCloseButton: true,
+        })).value;
+
+        if (!prop) {
+            return null;
+        }
+
+        prop = this.parseProp(prop);
+
+        let params = get_free_parameters(prop);
+        params = uniq(params);
+
+        const needSelectionNames = [];
+        for (const param of params) {
+            if (param.kind !== 'Uninstantiated') {
+                continue;
+            }
+
+            const paramName = param.value;
+
+            const paramAssumptions = assumptions
+                .filter((assumption) => assumption.assumption.ident.name === paramName);
+
+            if (paramAssumptions.length === 0) {
+                error(`Unknown identifier: ${paramName}`);
+                return null;
+            }
+
+            const datatypeParamAssumptions = paramAssumptions
+                .filter((assumption) => assumption.assumption.kind === 'Datatype');
+
+            if (datatypeParamAssumptions.length === 0) {
+                error(`Not a value: ${paramName}`);
+                return null;
+            }
+
+            if (datatypeParamAssumptions.length > 1) {
+                needSelectionNames.push(paramName);
+                continue;
+            }
+
+            prop = instantiate_free_parameter(prop, paramName, datatypeParamAssumptions[0].assumption.ident);
+        }
+
+        if (needSelectionNames.length === 0) {
+            return prop;
+        }
+
+        // prompt for user selection
+        const selectionOptions = needSelectionNames
+            .reduce((accu, name) => {
+                accu[name] = assumptions
+                    .filter((assumptions) => assumptions.assumption.ident.name === name)
+                    .map((assumption) => assumption.assumption.ident);
+
+                return accu;
+            }, {} as { [name: string]: Identifier[] });
+
+        let finalProp: Prop | null = null;
+        await ReactSwal.fire({
+            title: 'Please further specify which identifier you mean.',
+            html: React.createElement(VisualProofEditorParameterIdentifierSelector, {
+                prop,
+                options: selectionOptions,
+                onAllSelect: (prop) => { finalProp = prop; },
+                getPopupContainer: () => Swal.getContainer() || document.body,
+            }),
+        });
+
+        return finalProp;
+    }
+
     protected parseProp(prop: string): Prop {
         try {
             return parse_prop(prop);
diff --git a/frontend/src/util/print-prop.ts b/frontend/src/util/print-prop.ts
index 46b8d7b..6dee2ea 100644
--- a/frontend/src/util/print-prop.ts
+++ b/frontend/src/util/print-prop.ts
@@ -55,6 +55,11 @@ export function printProp(prop: Prop): string {
     const shouldWrapFst = (propPrecedence > fstPrecedence) || (propPrecedence === fstPrecedence && isRightAssociative(prop));
     const shouldWrapSnd = (propPrecedence > sndPrecedence) || (propPrecedence === sndPrecedence && isLeftAssociative(prop));
 
+    // Special rendering for A -> False
+    if (prop.kind === 'Impl' && snd.kind === 'False') {
+        const shoudlWrap = propPrecedence > fstPrecedence;
+        return `¬${wrap(fst, shoudlWrap)}`;
+    }
     return wrap(fst, shouldWrapFst) + ` ${connective} ` + wrap(snd, shouldWrapSnd);
 }
 
@@ -65,7 +70,13 @@ function getPrecedence(prop: Prop): number {
         case 'False': return 999;
         case 'And': return 4;
         case 'Or': return 3;
-        case 'Impl': return 2;
+        case 'Impl': {
+            if (prop.value[1].kind === 'False') {
+                return 999;
+            }
+
+            return 2;
+        }
         case 'ForAll': return 1;
         case 'Exists': return 1;
     }
diff --git a/src/kernel/prop.rs b/src/kernel/prop.rs
index 2596698..23de71f 100644
--- a/src/kernel/prop.rs
+++ b/src/kernel/prop.rs
@@ -271,6 +271,70 @@ impl Prop {
         }
     }
 
+    pub fn instantiate_free_parameter_by_index(&mut self, index: usize, substitutor: &Identifier) {
+        fn _instantiate<'a>(
+            prop: &'a mut Prop,
+            index: usize,
+            substitutor: &Identifier,
+            current_index: &mut usize,
+            bound_identifiers: &mut Vec<&'a str>,
+        ) {
+            match prop {
+                Prop::True => {}
+                Prop::False => {}
+                Prop::And(fst, snd) | Prop::Or(fst, snd) | Prop::Impl(fst, snd) => {
+                    _instantiate(
+                        fst,
+                        index,
+                        substitutor,
+                        current_index,
+                        &mut bound_identifiers.clone(),
+                    );
+
+                    if *current_index > index {
+                        return;
+                    }
+
+                    _instantiate(snd, index, substitutor, current_index, bound_identifiers);
+                }
+                Prop::ForAll {
+                    object_ident,
+                    ref mut body,
+                    ..
+                }
+                | Prop::Exists {
+                    object_ident,
+                    ref mut body,
+                    ..
+                } => {
+                    bound_identifiers.push(object_ident.as_str());
+
+                    _instantiate(body, index, substitutor, current_index, bound_identifiers);
+                }
+                Prop::Atom(_, params) => {
+                    let param_limit = index - *current_index + 1;
+                    if params.len() < param_limit {
+                        return;
+                    }
+
+                    let Some(param) = params.get_mut(index - *current_index) else {
+                        panic!("Invalid index.");
+                    };
+
+                    *param = PropParameter::Instantiated(substitutor.clone());
+                }
+            }
+        }
+
+        let mut current_index = 0;
+        _instantiate(self, index, substitutor, &mut current_index, &mut vec![]);
+
+        // sanity check
+        if current_index < index {
+            panic!("Proposition has not enough parameters.");
+        }
+    }
+
     // Warning: This might bind free (uninstantiated) parameters.
     // Choose bind name with care.
     pub fn bind_identifier(
@@ -1698,4 +1762,181 @@ mod tests {
             Err(InstatiationError::UnknownIdentifier("x".to_string()))
         );
     }
+
+    #[test]
+    fn test_instantiate_free_parameter_by_index_noop_on_true() {
+        let mut prop = Prop::True;
+        let subst = Identifier::new("sub".to_string(), 42);
+
+        prop.instantiate_free_parameter_by_index(0, &subst);
+
+        assert_eq!(prop, Prop::True);
+    }
+
+    #[test]
+    fn test_instantiate_free_parameter_by_index_noop_on_false() {
+        let mut prop = Prop::False;
+        let subst = Identifier::new("sub".to_string(), 42);
+
+        prop.instantiate_free_parameter_by_index(0, &subst);
+
+        assert_eq!(prop, Prop::False);
+    }
+
+    #[test]
+    fn test_instantiate_free_parameter_by_index_substitute_in_atom_single_param() {
+        let mut prop = Prop::Atom(
+            "A".to_string(),
+            vec![PropParameter::Uninstantiated("x".to_string())],
+        );
+        let subst = Identifier::new("sub".to_string(), 42);
+
+        prop.instantiate_free_parameter_by_index(0, &subst);
+
+        assert_eq!(
+            prop,
+            Prop::Atom(
+                "A".to_string(),
+                vec![PropParameter::Instantiated(Identifier::new(
+                    "sub".to_string(),
+                    42
+                ))]
+            )
+        );
+    }
+
+    #[test]
+    fn test_instantiate_free_parameter_by_index_substitute_in_atom_multi_params() {
+        let mut prop = Prop::Atom(
+            "A".to_string(),
+            vec![
+                PropParameter::Uninstantiated("x".to_string()),
+                PropParameter::Uninstantiated("y".to_string()),
+            ],
+        );
+        let subst = Identifier::new("sub".to_string(), 42);
+
+        prop.instantiate_free_parameter_by_index(1, &subst);
+
+        assert_eq!(
+            prop,
+            Prop::Atom(
+                "A".to_string(),
+                vec![
+                    PropParameter::Uninstantiated("x".to_string()),
+                    PropParameter::Instantiated(Identifier::new("sub".to_string(), 42))
+                ]
+            )
+        );
+    }
+
+    #[test]
+    #[should_panic(expected = "Proposition has not enough parameters.")]
+    fn test_instantiate_free_parameter_by_index_panic_on_invalid_index() {
+        let mut prop = Prop::Atom(
+            "A".to_string(),
+            vec![PropParameter::Uninstantiated("x".to_string())],
+        );
+        let subst = Identifier::new("sub".to_string(), 42);
+
+        prop.instantiate_free_parameter_by_index(10, &subst);
+    }
+
+    #[test]
+    fn test_instantiate_free_parameter_by_index_substitute_in_nested_and() {
+        let mut prop = Prop::And(
+            Box::new(Prop::Atom(
+                "A".to_string(),
+                vec![PropParameter::Uninstantiated("x".to_string())],
+            )),
+            Box::new(Prop::Atom(
+                "B".to_string(),
+                vec![PropParameter::Uninstantiated("y".to_string())],
+            )),
+        );
+        let subst = Identifier::new("sub".to_string(), 42);
+
+        prop.instantiate_free_parameter_by_index(1, &subst);
+
+        assert_eq!(
+            prop,
+            Prop::And(
+                Box::new(Prop::Atom(
+                    "A".to_string(),
+                    vec![PropParameter::Uninstantiated("x".to_string())],
+                )),
+                Box::new(Prop::Atom(
+                    "B".to_string(),
+                    vec![PropParameter::Instantiated(Identifier::new(
+                        "sub".to_string(),
+                        42
+                    ))],
+                )),
+            )
+        );
+    }
+
+    #[test]
+    fn test_instantiate_free_parameter_by_index_substitute_in_forall_body() {
+        let mut prop = Prop::ForAll {
+            object_ident: "x".to_string(),
+            object_type_ident: "t".to_string(),
+            body: Box::new(Prop::Atom(
+                "A".to_string(),
+                vec![PropParameter::Uninstantiated("x".to_string())],
+            )),
+        };
+        let subst = Identifier::new("sub".to_string(), 42);
+
+        prop.instantiate_free_parameter_by_index(0, &subst);
+
+        assert_eq!(
+            prop,
+            Prop::ForAll {
+                object_ident: "x".to_string(),
+                object_type_ident: "t".to_string(),
+                body: Box::new(Prop::Atom(
+                    "A".to_string(),
+                    vec![PropParameter::Instantiated(Identifier::new(
+                        "sub".to_string(),
+                        42
+                    ))],
+                )),
+            }
+        );
+    }
+
+    #[test]
+    #[should_panic(expected = "Proposition has not enough parameters.")]
+    fn test_instantiate_free_parameter_by_index_panic_when_index_too_large_for_atom() {
+        let mut prop = Prop::Atom(
+            "P".to_string(),
+            vec![PropParameter::Uninstantiated("x".to_string())],
+        );
+        let subst = Identifier::new("sub".to_string(), 42);
+
+        prop.instantiate_free_parameter_by_index(5, &subst);
+    }
+
+    #[test]
+    #[should_panic(expected = "Proposition has not enough parameters.")]
+    fn test_instantiate_free_parameter_by_index_panic_when_index_too_large_in_complex_prop() {
+        let mut prop = Prop::And(
+            Box::new(Prop::Atom(
+                "A".to_string(),
+                vec![PropParameter::Uninstantiated("x".to_string())],
+            )),
+            Box::new(Prop::ForAll {
+                object_ident: "y".to_string(),
+                object_type_ident: "t".to_string(),
+                body: Box::new(Prop::Atom(
+                    "B".to_string(),
+                    vec![PropParameter::Uninstantiated("z".to_string())],
+                )),
+            }),
+        );
+        let subst = Identifier::new("sub".to_string(), 42);
+
+        prop.instantiate_free_parameter_by_index(10, &subst);
+    }
 }
diff --git a/src/lib.rs b/src/lib.rs
index 887b4c3..168088c 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -154,6 +154,16 @@ pub fn instantiate_free_parameter(
     prop
 }
 
+#[wasm_bindgen]
+pub fn instantiate_free_parameter_by_index(
+    mut prop: Prop,
+    index: usize,
+    substitutor: &Identifier,
+) -> Prop {
+    prop.instantiate_free_parameter_by_index(index, substitutor);
+    prop
+}
+
 #[wasm_bindgen]
 pub fn bind_identifier(
     prop: &Prop,